# Documentation

Mathlib.GroupTheory.Perm.Option

# 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 ()) :
= 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.fst * Equiv.optionCongr i.snd

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

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.toEmbedding Equiv.Perm.decomposeOption.symm) 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.