add_self — Mathlib

English

In a Boolean ring, doubling a element yields zero: a + a = 0 for all a.

Русский

В булевом кольце сложение с самим собой даёт ноль: a + a = 0.

LaTeX

$$$$ a + a = 0. $$$$

Lean4

@[scoped simp]
theorem add_self : a + a = 0 :=
  by
  have : a + a = a + a + (a + a) :=
    calc
      a + a = (a + a) * (a + a) := by rw [mul_self]
      _ = a * a + a * a + (a * a + a * a) := by rw [add_mul, mul_add]
      _ = a + a + (a + a) := by rw [mul_self]
  rwa [right_eq_add] at this

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