mathlib

17448c64 - feat(group_theory/perm/sign): induced permutation on a subtype that is a fintype (#5706)

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. Co-authored-by: paulvanwamelen <30371019+paulvanwamelen@users.noreply.github.com>