Commit 2020-12-15 10:30 dd72a981

View on Github →

feat(group_theory/perm/basic): Bundle sigma_congr_right and sum_congr into monoid_homs (#5301) This makes the corresponding subgroups available as monoid_hom.range. As a result, the old subgroup definitions can be removed. This also adds injectivity and cardinality lemmas.

Estimated changes

Modified src/group_theory/perm/basic.lean

added def equiv.perm.sigma_congr_right_hom

added theorem equiv.perm.sigma_congr_right_hom_injective

modified theorem equiv.perm.sigma_congr_right_inv

modified theorem equiv.perm.sigma_congr_right_mul

modified theorem equiv.perm.sigma_congr_right_one

added def equiv.perm.sum_congr_hom

added theorem equiv.perm.sum_congr_hom_injective

Modified src/group_theory/perm/subgroup.lean

added theorem equiv.perm.sigma_congr_right_hom.card_range

deleted def equiv.perm.sigma_congr_right_subgroup

added theorem equiv.perm.sum_congr_hom.card_range

deleted def equiv.perm.sum_congr_subgroup