mathlib documentation

group_theory.perm.option

Permutations of option α #

@[simp]
theorem equiv_functor.option.map_none {α β : Type u_1} (e : α β) :
@[simp]
theorem map_equiv_option_one {α : Type u_1} :
@[simp]
@[simp]
theorem map_equiv_option_swap {α : Type u_1} [decidable_eq α] (x y : α) :

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

Equations

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