English
Under appropriate semiring conditions, the idempotence of a + b is equivalent to a b + b a = 0 when a and b are idempotent.
Русский
При надлежащих условиях полугруппы, идемпотентность a + b эквивалентна ab + ba = 0 при идемпотентности a и b.
LaTeX
$$IsIdempotentElem (a + b) \Leftrightarrow a b + b a = 0.$$
Lean4
/-- `a + b` is idempotent if and only if `a` and `b` anti-commute. -/
theorem add_iff [NonUnitalNonAssocSemiring R] [IsCancelAdd R] {a b : R} (ha : IsIdempotentElem a)
(hb : IsIdempotentElem b) : IsIdempotentElem (a + b) ↔ a * b + b * a = 0 :=
by
refine ⟨fun h ↦ ?_, ha.add hb⟩
rw [← add_right_cancel_iff (a := b), add_assoc, ← add_left_cancel_iff (a := a), ← add_assoc, add_add_add_comm]
simpa [add_mul, mul_add, ha.eq, hb.eq] using h.eq
