# Permutations of Option α#

@[simp]
theorem Equiv.optionCongr_one {α : Type u_1} :
@[simp]
theorem Equiv.optionCongr_swap {α : Type u_1} [] (x : α) (y : α) :
@[simp]
theorem Equiv.optionCongr_sign {α : Type u_1} [] [] (e : ) :
Equiv.Perm.sign = Equiv.Perm.sign e
@[simp]
theorem map_equiv_removeNone {α : Type u_1} [] (σ : Equiv.Perm ()) :
().optionCongr = Equiv.swap none (σ none) * σ
@[simp]
theorem Equiv.Perm.decomposeOption_apply {α : Type u_1} [] (σ : Equiv.Perm ()) :
Equiv.Perm.decomposeOption σ = (σ none, )
@[simp]
theorem Equiv.Perm.decomposeOption_symm_apply {α : Type u_1} [] (i : ) :
Equiv.Perm.decomposeOption.symm i = Equiv.swap none i.1 *

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Equiv.Perm.decomposeOption_symm_of_none_apply {α : Type u_1} [] (e : ) (i : ) :
(Equiv.Perm.decomposeOption.symm (none, e)) i = Option.map (e) i
theorem Equiv.Perm.decomposeOption_symm_sign {α : Type u_1} [] [] (e : ) :
Equiv.Perm.sign (Equiv.Perm.decomposeOption.symm (none, e)) = Equiv.Perm.sign e
theorem Finset.univ_perm_option {α : Type u_1} [] [] :
Finset.univ = Finset.map Equiv.Perm.decomposeOption.symm.toEmbedding Finset.univ

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