Commit 2022-10-16 01:04 71a759b2

View on Github →

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.

Estimated changes

Modified src/group_theory/subgroup/basic.lean

added theorem monoid_hom.restrict_ker

added theorem monoid_hom.restrict_range

Modified src/group_theory/submonoid/operations.lean

added theorem monoid_hom.restrict_mker

added theorem monoid_hom.restrict_mrange