add_eq_zero'

Mathlib.Algebra.Ring.BooleanRing

URI: https://scilib.ai/kg/mathlib#BooleanRing.add_eq_zero'

English

In a Boolean ring, a + b = 0 if and only if a = b.

Русский

В булевом кольце a + b = 0 тогда, когда a = b.

LaTeX

$$$$ a + b = 0 \\iff a = b. $$$$

Lean4

theorem add_eq_zero' : a + b = 0 ↔ a = b :=
  calc
    a + b = 0 ↔ a = -b := add_eq_zero_iff_eq_neg
    _ ↔ a = b := by rw [neg_eq]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru