Theorem IsIdempotentElem.add_sub_mul_of_commute

Modification history

2025-07-31 05:15
Mathlib/Algebra/Ring/Idempotent.lean
feat(Algebra/Ring/Idempotent): subtraction lemmas for idempotents and star projections (#25910) …
Modified IsIdempotentElem.add_sub_mul_of_commuteView on Github →
2025-01-15 07:14
Mathlib/Algebra/Ring/Idempotent.lean
chore(Idempotent): split into `Group`, `GroupWithZero` and `Ring` parts (#20742) …
Modified IsIdempotentElem.add_sub_mul_of_commuteView on Github →
2024-11-25 16:30
Mathlib/Algebra/Ring/Idempotents.lean
feat: ring with discrete PrimeSpectrum (#18891) …
Added IsIdempotentElem.add_sub_mul_of_commuteView on Github →