Commit 2026-03-26 17:12 f7c5c08f

View on Github →

feat(Algebra/Group): some API lemmas for powMonoidHom (#36458) This adds a few lemmas about powMonoidHom/nsmulAddMonoidHom and one convenience lemma that says that the range (as a MonoidHom/AddMonoidHom) of a MulEquiv/AddEquiv is the top subobject. It also defines the isomorphism ((i : ι) → A i) ⧸ (powMonoidHom n).range ≃* ((i : ι) → A i ⧸ (powMonoidHom n).range) and its additive version.

Estimated changes

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

added theorem MulEquiv.map_range_powMonoidHom

added theorem MulEquiv.range_eq_top

added theorem Subgroup.subgroupOf_map_powMonoidHom_eq_range

Modified Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean

modified theorem Int.range_castAddHom

added theorem Int.range_nsmulAddMonoidHom

Modified Mathlib/GroupTheory/QuotientGroup/Basic.lean

added def QuotientGroup.mulEquivPiModRangePowMonoidHom

added theorem QuotientGroup.mulEquivPiModRangePowMonoidHom_apply