add — Mathlib

English

If a and b are idempotent and a and b anti-commute up to sign (hab: ab + ba = 0), then a + b is idempotent.

Русский

Если a и b идемпотентны и антикоммутируют в знаковом смысле (ab+ba=0), то a+b идемпотентно.

LaTeX

$$If ha, hb are idempotent and hab: a b + b a = 0, then IsIdempotentElem (a + b).$$

Lean4

/-- `a + b` is idempotent when `a` and `b` anti-commute. -/
theorem add [NonUnitalNonAssocSemiring R] {a b : R} (ha : IsIdempotentElem a) (hb : IsIdempotentElem b)
    (hab : a * b + b * a = 0) : IsIdempotentElem (a + b) := by
  simp_rw [IsIdempotentElem, mul_add, add_mul, ha.eq, hb.eq, add_add_add_comm, ← add_assoc, add_assoc a, hab, zero_add]

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