mathlib

dbb5ca1e - refactor(group_theory/perm): move perm.subtype_perm to basic (#6005)

refactor(group_theory/perm): move perm.subtype_perm to basic (#6005) Both `perm.subtype_perm` and `perm.of_subtype` can be moved up the import hierarchy out of `group_theory/perm/sign` since they do not rely on any finiteness assumption.