`mul`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.ArithmeticFromLogic on GitHub at line 171.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 168    rw [add_succ, succ_add, ih]
 169
 170/-- Multiplication by recursion on the second argument. -/
 171def mul : LogicNat → LogicNat → LogicNat
 172  | _, .identity => zero
 173  | n, .step m   => mul n m + n
 174
 175instance : Mul LogicNat := ⟨mul⟩
 176
 177@[simp] theorem mul_def (n m : LogicNat) : n * m = mul n m := rfl
 178
 179@[simp] theorem mul_zero (n : LogicNat) : n * zero = zero := rfl
 180
 181@[simp] theorem mul_succ (n m : LogicNat) : n * succ m = n * m + n := rfl
 182
 183theorem zero_mul (n : LogicNat) : zero * n = zero := by
 184  induction n with
 185  | identity => rfl
 186  | step n ih =>
 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]

papers checked against this theorem

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