Theorem bijective_pi_of_isIdempotentElem

Modification history

2025-05-02 14:55
Mathlib/RingTheory/Idempotents.lean
feat(RingTheory/Idempotents): binary version of `bijective_pi_of_isIdempotentElem` (#24518) …
Deleted bijective_pi_of_isIdempotentElemView on Github →
2024-07-25 00:13
Mathlib/RingTheory/Idempotents.lean
feat(RingTheory/Idempotents): Lifting complete orthogonal idempotents along nil extensions (#14372)
Added bijective_pi_of_isIdempotentElemView on Github →