mathlib documentation


Lemmas about subgroups within the permutations (self-equivalences) of a type α #

This file provides extra lemmas about some subgroups that exist within equiv.perm α. group_theory.subgroup depends on group_theory.perm.basic, so these need to be in a separate file.

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 quotient_group.quotient of these subgroups.

def equiv.perm.sum_congr_hom.decidable_mem_range {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] :
def equiv.perm.sigma_congr_right_hom.decidable_mem_range {α : Type u_1} {β : α → Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (β a)] [fintype α] [Π (a : α), fintype (β a)] :
decidable_pred (λ (x : equiv.perm (Σ (a : α), β a)), x (equiv.perm.sigma_congr_right_hom β).range)
theorem equiv.perm.sigma_congr_right_hom.card_range {α : Type u_1} {β : α → Type u_2} [fintype ((equiv.perm.sigma_congr_right_hom β).range)] [fintype (Π (a : α), equiv.perm (β a))] :