add_eq_zero — Mathlib

English

Let R be a ring of characteristic two. For all a,b in R, a + b = 0 if and only if a = b.

Русский

Пусть R — кольцо характеристикой 2. Для любых a,b ∈ R выполняется a + b = 0 тогда и только тогда, когда a = b.

LaTeX

$$$(\\\\operatorname{ringChar}(R) = 2) \\\\\\Rightarrow \\\\forall a,b \\\\in R,\\\\ a+b=0 \\\\iff a=b $$$

Lean4

protected theorem add_eq_zero {a b : R} : a + b = 0 ↔ a = b := by rw [← CharTwo.sub_eq_add, sub_eq_iff_eq_add, zero_add]

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