Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-16 14:09 e00d688f

View on Github →

chore(group_theory/subgroup): rename monoid_hom.to_range to monoid_hom.range_restrict (#7218) This makes it match:

monoid_hom.mrange_restrict
linear_map.range_restrict
ring_hom.range_restrict
ring_hom.srange_restrict
alg_hom.range_restrict This also adds a missing simp lemma.

Estimated changes

Modified src/algebra/category/Group/images.lean

modified def AddCommGroup.factor_thru_image

Modified src/group_theory/quotient_group.lean

Modified src/group_theory/subgroup.lean

added theorem monoid_hom.coe_range_restrict

added def monoid_hom.range_restrict

added theorem monoid_hom.range_restrict_ker

deleted def monoid_hom.to_range

deleted theorem monoid_hom.to_range_ker