Documentation

Mathlib.GroupTheory.Perm.Option

Permutations of Option α #

source
@[simp]
theorem Equiv.optionCongr_one {α : Type u_1} :
optionCongr 1 = 1
source
@[simp]
theorem Equiv.optionCongr_swap {α : Type u_1} [DecidableEq α] (x y : α) :
optionCongr (swap x y) = swap (some x) (some y)
source
@[simp]
theorem Equiv.optionCongr_sign {α : Type u_1} [DecidableEq α] [Fintype α] (e : Perm α) :
Perm.sign (optionCongr e) = Perm.sign e
source
@[simp]
theorem map_equiv_removeNone {α : Type u_1} [DecidableEq α] (σ : Equiv.Perm (Option α)) :
(Equiv.removeNone σ).optionCongr = Equiv.swap none (σ none) * σ
source
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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Equiv.Perm.decomposeOption_apply {α : Type u_1} [DecidableEq α] (σ : Perm (Option α)) :
    decomposeOption σ = (σ none, removeNone σ)
    source
    @[simp]
    theorem Equiv.Perm.decomposeOption_symm_apply {α : Type u_1} [DecidableEq α] (i : Option α × Perm α) :
    decomposeOption.symm i = swap none i.1 * optionCongr i.2
    source
    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
    source
    theorem Equiv.Perm.decomposeOption_symm_sign {α : Type u_1} [DecidableEq α] [Fintype α] (e : Perm α) :
    sign (decomposeOption.symm (none, e)) = sign e
    source
    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.