Permutations of Option α

@[simp]

theorem Equiv.optionCongr_one {α : Type u_1} : optionCongr 1 = 1

@[simp]

theorem Equiv.optionCongr_swap {α : Type u_1} [DecidableEq α] (x y : α) : optionCongr (swap x y) = swap (some x) (some y)

@[simp]

theorem Equiv.optionCongr_sign {α : Type u_1} [DecidableEq α] [Fintype α] (e : Perm α) : Perm.sign (optionCongr e) = Perm.sign e

@[simp]

theorem map_equiv_removeNone {α : Type u_1} [DecidableEq α] (σ : Equiv.Perm (Option α)) : (Equiv.removeNone σ).optionCongr = Equiv.swap none (σ none) * σ

def Equiv.Perm.decomposeOption {α : Type u_1} [DecidableEq α] : Perm (Option α) ≃ Option α × Perm α

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

@[simp]

theorem Equiv.Perm.decomposeOption_symm_apply {α : Type u_1} [DecidableEq α] (i : Option α × Perm α) : decomposeOption.symm i = swap none i.1 * optionCongr i.2

@[simp]

theorem Equiv.Perm.decomposeOption_apply {α : Type u_1} [DecidableEq α] (σ : Perm (Option α)) : decomposeOption σ = (σ none, removeNone σ)

theorem Equiv.Perm.decomposeOption_symm_of_none_apply {α : Type u_1} [DecidableEq α] (e : Perm α) (i : Option α) : (decomposeOption.symm (none, e)) i = Option.map (⇑e) i

theorem Equiv.Perm.decomposeOption_symm_sign {α : Type u_1} [DecidableEq α] [Fintype α] (e : Perm α) : sign (decomposeOption.symm (none, e)) = sign e

theorem Finset.univ_perm_option {α : Type u_1} [DecidableEq α] [Fintype α] : univ = map Equiv.Perm.decomposeOption.symm.toEmbedding 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.