`IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitMulBalancedZeroOfBalancedZeroRightChoiceFree`

IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/Grow/SignedOrbitMulBalancedZeroOfBalancedZeroRightChoiceFree.lean · 21 lines · 1 declarations

show as: view math explainer →

open module explainer GitHub source

Explainer status: ready · generated 2026-08-13 16:49:59.981955+00:00

   1import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational
   2import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder
   3import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitLeReflTotal
   4import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Orbit
   5
   6namespace IndisputableMonolith.PRCGrow.SignedOrbitMulBalancedZeroOfBalancedZeroRightChoiceFree
   7
   8open IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus
   9
  10theorem mul_balanced_zero_of_balanced_zero_right_cf
  11    (z w : SignedOrbit)
  12    (hw : w.balanced SignedOrbit.zero) :
  13    (z.mul w).balanced SignedOrbit.zero := by
  14  rw [SignedOrbit.balanced_iff_toNat_eq] at hw ⊢
  15  simp only [SignedOrbit.mul_pos, SignedOrbit.mul_neg, SignedOrbit.zero,
  16    DistinctionNat.toNat_add, DistinctionNat.toNat_mul, DistinctionNat.toNat_zero,
  17    Nat.add_zero, Nat.zero_add] at hw ⊢
  18  rw [hw]
  19
  20end IndisputableMonolith.PRCGrow.SignedOrbitMulBalancedZeroOfBalancedZeroRightChoiceFree
  21

source mirrored from github.com/jonwashburn/shape-of-logic