`mul_one`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.ArithmeticFromLogic
domain: Foundation
line: 190 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.ArithmeticFromLogic on GitHub at line 190.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 187    show zero * succ n = zero
 188    rw [mul_succ, ih, zero_add]
 189
 190theorem mul_one (n : LogicNat) : n * succ zero = n := by
 191  show n * succ zero = n
 192  rw [mul_succ, mul_zero, zero_add]
 193
 194theorem one_mul (n : LogicNat) : succ zero * n = n := by
 195  induction n with
 196  | identity => rfl
 197  | step n ih =>
 198    show succ zero * succ n = succ n
 199    rw [mul_succ, ih]
 200    show n + succ zero = succ n
 201    rw [add_succ, add_zero]
 202
 203theorem mul_add (a b c : LogicNat) : a * (b + c) = a * b + a * c := by
 204  induction c with
 205  | identity =>
 206    show a * (b + zero) = a * b + a * zero
 207    rw [add_zero, mul_zero, add_zero]
 208  | step c ih =>
 209    show a * (b + succ c) = a * b + a * succ c
 210    rw [add_succ, mul_succ, mul_succ, ih, add_assoc]
 211
 212/-! ## 5. Recovery Theorem: LogicNat ≃ Nat
 213
 214Lean's built-in `Nat` has the same inductive shape as `LogicNat`. The
 215two are isomorphic. This is the recovery: the natural numbers Lean
 216already has are exactly the structure forced by the Law of Logic, with
 217no base 10, no positional representation, and no arithmetic axioms
 218posited. -/
 219
 220/-- The forward map: read off the iteration count. -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.