Theorem RingHom.prod_bijective_of_isIdempotentElem

Modification history

2025-05-02 14:55

Mathlib/RingTheory/Idempotents.lean

feat(RingTheory/Idempotents): binary version of `bijective_pi_of_isIdempotentElem` (#24518) …

Added RingHom.prod_bijective_of_isIdempotentElem View on Github →