Theorems · Theorem · commutative algebra

IsIdempotentElem.add_iff

∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] [IsCancelAdd R] {a b : R},
  IsIdempotentElem a → IsIdempotentElem b → (IsIdempotentElem (a + b) ↔ a * b + b * a = 0)

a + b is idempotent if and only if a and b anti-commute.

Defined in

Mathlib.Algebra.Ring.Idempotent

Cited by

1 results in Mathlib

Foundations

Depth 9 from the axioms · uses propext

Assumes

NonUnitalNonAssocSemiringIsCancelAdd