Theorems · Theorem · commutative algebra

IsIdempotentElem.sub

∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] {a b : R},
  IsIdempotentElem a → IsIdempotentElem b → a * b = a → b * a = a → IsIdempotentElem (b - a)

b - a is idempotent when a * b = a and b * a = a.

Defined in

Mathlib.Algebra.Ring.Idempotent

Cited by

3 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext

Assumes

NonUnitalNonAssocRing