Commit 2021-02-09 11:14 17448c64

feat(group_theory/perm/sign): induced permutation on a subtype that is a fintype (#5706) If a permutation on a type maps a subtype into itself and the subtype is a fintype, then we get a permutation on the subtype. Similar to the subtype_perm definition in the same file.