mathlibdocumentation

group_theory.perm.option

Permutations of option α#

@[simp]
theorem equiv.option_congr_one {α : Type u_1} :
@[simp]
theorem equiv.option_congr_swap {α : Type u_1} [decidable_eq α] (x y : α) :
@[simp]
theorem equiv.option_congr_sign {α : Type u_1} [decidable_eq α] [fintype α] (e : equiv.perm α) :
@[simp]
theorem map_equiv_remove_none {α : Type u_1} [decidable_eq α] (σ : equiv.perm (option α)) :
def equiv.perm.decompose_option {α : Type u_1} [decidable_eq α] :

Permutations of option α are equivalent to fixing an option α and permuting the remaining with a perm α. The fixed option α is swapped with none.

Equations
@[simp]
theorem equiv.perm.decompose_option_apply {α : Type u_1} [decidable_eq α] (σ : equiv.perm (option α)) :
@[simp]
theorem equiv.perm.decompose_option_symm_apply {α : Type u_1} [decidable_eq α] (i : × ) :
theorem equiv.perm.decompose_option_symm_sign {α : Type u_1} [decidable_eq α] [fintype α] (e : equiv.perm α) :
theorem finset.univ_perm_option {α : Type u_1} [decidable_eq α] [fintype α] :

The set of all permutations of option α can be constructed by augmenting the set of permutations of α by each element of option α in turn.