mathlib

f3101e82 - feat(group_theory/perm/basic): permutations of a subtype (#8691)

feat(group_theory/perm/basic): permutations of a subtype (#8691) This is the same as `(equiv.refl _)^.set.compl .symm.trans (subtype_equiv_right $ by simp)` (up to a `compl`) but with better unfolding.