add_self_eq_zero — Mathlib

English

If R is a NoZeroDivisors ring and CharZero, then for every a ∈ R, a + a = 0 if and only if a = 0.

Русский

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

LaTeX

$$$(\\forall a \\in R):\\ a + a = 0 \\iff a = 0$$$

Lean4

@[simp]
theorem add_self_eq_zero {a : R} : a + a = 0 ↔ a = 0 := by
  simp only [(two_mul a).symm, mul_eq_zero, two_ne_zero, false_or]

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