Theorem RingCon.mkₐ_comp_factorₐ_comp_mkₐ

Modification history

2025-11-26 15:01
Mathlib/RingTheory/Congruence/Hom.lean
feat(RingTheory/Congruence/Hom): prove basic isomorphisms theorems for ring congruences (#26277) …
Added RingCon.mkₐ_comp_factorₐ_comp_mkₐView on Github →