Commit 2021-09-01 19:25 07c57b56

View on Github →

feat(group_theory): Add monoid_hom.mker and generalise the codomain for monoid_hom.ker (#8532) Add monoid_hom.mker for f : M ->* N, where M and N are mul_one_classes, and monoid_hom.ker is now defined for f : G ->* H, where H is a mul_one_class

Estimated changes

Modified src/group_theory/subgroup.lean

modified theorem monoid_hom.coe_ker

modified def monoid_hom.ker

modified theorem monoid_hom.ker_one

modified theorem monoid_hom.mem_ker

Modified src/group_theory/submonoid/operations.lean

added theorem monoid_hom.coe_mker

added theorem monoid_hom.comap_bot'

added theorem monoid_hom.comap_mker

added theorem monoid_hom.mem_mker

added def monoid_hom.mker

added theorem monoid_hom.mker_one

added theorem monoid_hom.mker_prod_map

added theorem monoid_hom.prod_map_comap_prod'

added theorem monoid_hom.range_restrict_mker