add_mul_succ — Mathlib

English

(a + b) · succ c = a · succ c + b under ba: b + a = a.

Русский

(a + b) · succ c = a · succ c + b при ba: b + a = a.

LaTeX

$$$\forall a,b,c \in \mathrm{Ordinal},\ ba:\ b + a = a \rightarrow (a + b) \cdot \mathrm{succ}(c) = a \cdot \mathrm{succ}(c) + b$$$

Lean4

theorem add_mul_succ {a b : Ordinal} (c) (ba : b + a = a) : (a + b) * succ c = a * succ c + b := by
  induction c using limitRecOn with
  | zero => simp only [succ_zero, mul_one]
  | succ c IH => rw [mul_succ, IH, ← add_assoc, add_assoc _ b, ba, ← mul_succ]
  | limit c l IH => rw [mul_succ, add_mul_limit_aux ba l IH, mul_succ, add_assoc]

Похожие утверждения