Lemmas about subgroups within the permutations (self-equivalences) of a type
It also provides decidable instances on membership in these subgroups, since
monoid_hom.decidable_mem_range cannot be inferred without the help of a lambda.
The presence of these instances induces a
fintype instance on the
- equiv.perm.sigma_congr_right_hom.decidable_mem_range = λ (x : equiv.perm (Σ (a : α), β a)), infer_instance