mathlib

dd72a981 - feat(group_theory/perm/basic): Bundle sigma_congr_right and sum_congr into monoid_homs (#5301)

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.