Documentation

Mathlib.GroupTheory.Perm.Option

Permutations of Option α #

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

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} [DecidableEq α] (e : Equiv.Perm α) (i : Option α) :
    (Equiv.Perm.decomposeOption.symm (none, e)) i = Option.map (⇑e) i
    theorem Equiv.Perm.decomposeOption_symm_sign {α : Type u_1} [DecidableEq α] [Fintype α] (e : Equiv.Perm α) :
    Equiv.Perm.sign (Equiv.Perm.decomposeOption.symm (none, e)) = Equiv.Perm.sign e
    theorem Finset.univ_perm_option {α : Type u_1} [DecidableEq α] [Fintype α] :
    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.