Mathlib Changelog
v4
Changelog
About
Github
Theorem
isIdempotentElem_one_sub_one_sub_pow_pow
Modification history
2024-07-25 00:13
Mathlib/RingTheory/Idempotents.lean
feat(RingTheory/Idempotents): Lifting complete orthogonal idempotents along nil extensions (#14372)
Added
isIdempotentElem_one_sub_one_sub_pow_pow
View on Github →