add_eq_zero_iff — Mathlib

English

Sum to zero characterizes zeros: a + b = 0 iff a = 0 and b = 0.

Русский

Сумма равна нулю тогда и только тогда, когда оба слагаемых равны нулю.

LaTeX

$$$a,b \in \mathrm{Ordinal} \Rightarrow a+b=0 \iff a=0 \land b=0$$$

Lean4

theorem add_eq_zero_iff {a b : Ordinal} : a + b = 0 ↔ a = 0 ∧ b = 0 :=
  inductionOn₂ a b fun α r _ β s _ =>
    by
    simp_rw [← type_sum_lex, type_eq_zero_iff_isEmpty]
    exact isEmpty_sum

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