mathlib3

4f4e7fa6 - feat(group_theory/perm/basic): `subtype_perm` is a monoid hom (#17816)

feat(group_theory/perm/basic): `subtype_perm` is a monoid hom (#17816) A few more `subtype_perm` lemmas. Clean up the `subtype_perm` section. Rename `equiv.perm.default_perm` to `equiv.perm.default_eq`.