mathlib3
e00d688f - chore(group_theory/subgroup): rename `monoid_hom.to_range` to `monoid_hom.range_restrict` (#7218)

Commit
4 years ago
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.
Author
Parents
Loading