Commit 2025-05-02 14:55 f50e1520

View on Github →

feat(RingTheory/Idempotents): binary version of bijective_pi_of_isIdempotentElem (#24518) Also renames bijective_pi_of_isIdempotentElem to RingHom.pi_bijective_of_isIdempotentElem.

Estimated changes