Commit 2024-11-27 11:08 01b31e1d

View on Github →

chore(Submonoid/Subgroup): rename subtype_range to range_subtype (#19518) This matches the naming convention.

Estimated changes

Modified Mathlib/Algebra/DirectSum/Basic.lean

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

added theorem MonoidHom.range_comp

added theorem Subgroup.range_subtype

deleted theorem Subgroup.subtype_range

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

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

added theorem MonoidHom.mrange_comp

added theorem MonoidHom.mrange_eq_top

deleted theorem MonoidHom.mrange_eq_top_iff_surjective

added theorem Submonoid.mrange_subtype

deleted theorem Submonoid.range_subtype

Modified Mathlib/GroupTheory/Congruence/Basic.lean

Modified Mathlib/GroupTheory/Finiteness.lean

Modified Mathlib/GroupTheory/Index.lean

Modified Mathlib/GroupTheory/PGroup.lean

Modified Mathlib/GroupTheory/SchurZassenhaus.lean

Modified Mathlib/GroupTheory/SpecificGroups/Alternating.lean

Modified Mathlib/GroupTheory/Sylow.lean