Commit 2025-04-14 22:08 18ce4d81

View on Github →

chore(GroupTheory/Congruence): deduplicate ker and mulKer (#23244) This deprecates Con.mulKer and defines it in terms of ker (instead of vice versa). It's not entirely clear to me that MulHomClass is the way to go due to a lack of a coherent simp-normal form, but we can always switch to MulHom later. The signature of Con.mapOfSurjective has changed as a result. Zulip thread: #mathlib4 > Con.ker vs Con.mulKer @ 💬

Estimated changes

Modified Mathlib/GroupTheory/Congruence/Defs.lean

deleted def Con.correspondence

deleted def Con.mapGen

deleted def Con.mapOfSurjective

deleted theorem Con.mapOfSurjective_eq_mapGen

deleted def Con.mulKer

deleted theorem Con.mul_ker_mk_eq

Modified Mathlib/GroupTheory/Congruence/Hom.lean

added def Con.correspondence

modified def Con.ker

added theorem Con.ker_coeMulHom

added theorem Con.ker_mkMulHom_eq

modified theorem Con.ker_rel

added def Con.mapGen

added def Con.mapOfSurjective

added theorem Con.mapOfSurjective_eq_mapGen

modified def Con.mk'

added def Con.mkMulHom

added theorem Con.mul_ker_mk_eq