basic): Range and kernel of `monoid_hom.restrict` (#16988)

Commit

3 years ago

feat(group_theory/subgroup/basic): Range and kernel of `monoid_hom.restrict` (#16988) This PRs adds simp-lemmas for the range and kernel of `monoid_hom.restrict`.

Author

tb65536

Parents

4d8fe495

mathlib3 71a759b2 - feat(group_theory/subgroup/basic): Range and kernel of `monoid_hom.restrict` (#16988)

mathlib3
71a759b2 - feat(group_theory/subgroup/basic): Range and kernel of `monoid_hom.restrict` (#16988)