Commit 2026-01-26 17:29 4fdaa878

View on Github →

feat(Subgroup/Ker): generalize codomain in some lemmas (#34429) These lemmas work if the codomain is a MulOneClass, not necessarily a group.

Estimated changes

Modified Mathlib/Algebra/Group/Subgroup/Ker.lean

modified theorem MonoidHom.div_mem_ker_iff

modified theorem MonoidHom.ker_restrict

modified theorem MonoidHom.range_le_ker_iff