`zero_add`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.ArithmeticFromLogic
domain: Foundation
line: 140 · 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 140.

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

 137
 138@[simp] theorem add_succ (n m : LogicNat) : n + succ m = succ (n + m) := rfl
 139
 140theorem zero_add (n : LogicNat) : zero + n = n := by
 141  induction n with
 142  | identity => rfl
 143  | step n ih =>
 144    show zero + succ n = succ n
 145    rw [add_succ, ih]
 146
 147theorem succ_add (n m : LogicNat) : succ n + m = succ (n + m) := by
 148  induction m with
 149  | identity => rfl
 150  | step m ih =>
 151    show succ n + succ m = succ (n + succ m)
 152    rw [add_succ, add_succ, ih]
 153
 154theorem add_assoc (a b c : LogicNat) : (a + b) + c = a + (b + c) := by
 155  induction c with
 156  | identity => rfl
 157  | step c ih =>
 158    show (a + b) + succ c = a + (b + succ c)
 159    rw [add_succ, add_succ, add_succ, ih]
 160
 161theorem add_comm (a b : LogicNat) : a + b = b + a := by
 162  induction b with
 163  | identity =>
 164    show a + zero = zero + a
 165    rw [add_zero, zero_add]
 166  | step b ih =>
 167    show a + succ b = succ b + a
 168    rw [add_succ, succ_add, ih]
 169
 170/-- Multiplication by recursion on the second argument. -/

papers checked against this theorem

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