Commit 2025-04-30 10:47 d31099de

View on Github →

feat(QuotientGroup): surjectivity and kernel of QuotientGroup.map (#23205) Prove formulas for the kernel of QuotientGroup.lift and QuotientGroup.map and that these maps are surjective if the corresponding functions are surjective.

Estimated changes

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

modified theorem MonoidHom.comap_ker

added theorem MonoidHom.ker_toSubmonoid

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

added theorem Subgroup.map_toSubmonoid

Modified Mathlib/Algebra/Group/Submonoid/Operations.lean

added theorem Submonoid.map_comap_eq_self_of_surjective

Modified Mathlib/Data/Quot.lean

added theorem Quotient.lift_surjective

added theorem Quotient.lift_surjective_iff

Modified Mathlib/GroupTheory/QuotientGroup/Defs.lean

added theorem QuotientGroup.ker_lift

added theorem QuotientGroup.ker_map

added theorem QuotientGroup.lift_comp_mk'

added theorem QuotientGroup.lift_surjective_of_surjective

added theorem QuotientGroup.map_surjective_of_surjective