pith. machine review for the scientific record. sign in
theorem proved term proof

mul_add

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 203theorem mul_add (a b c : LogicNat) : a * (b + c) = a * b + a * c := by

proof body

Term-mode proof.

 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. -/

used by (15)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (25)

Lean names referenced from this declaration's body.