Theorems · Definition · group theory
Equiv.Perm.decomposeOption
{α : Type u_1} → [DecidableEq α] → Equiv.Perm (Option α) ≃ Option α × Equiv.Perm αPermutations of Option α are equivalent to fixing an
Option α and permuting the remaining with a Perm α.
The fixed Option α is swapped with none.
- Defined in
- Mathlib.GroupTheory.Perm.Option
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Equivstatement · cited by 8,337
- Equiv.Permstatement and proof · cited by 1,375
- Equiv.swapproof · cited by 197
- Equiv.optionCongrproof · cited by 19
- Equiv.removeNoneproof · cited by 10
Cited by13
Results whose statement or proof uses this declaration.
- Equiv.Perm.decomposeFinproof · cited by 9
- Equiv.Perm.decomposeOption_symm_applystatement and proof · cited by 7
- derangements.Equiv.RemoveNone.fiberproof · cited by 4
- Equiv.Perm.decomposeFin_symm_apply_succproof · cited by 3
- Equiv.Perm.decomposeFin.symm_signproof · cited by 2
- Equiv.Perm.decomposeFin_symm_apply_zeroproof · cited by 2
- Equiv.Perm.decomposeFin_symm_of_reflproof · cited by 2
- Equiv.Perm.decomposeOption_applystatement and proof · cited by 1
- derangements.Equiv.RemoveNone.fiber_someproof · cited by 0
- derangements.derangementsOptionEquivSigmaAtMostOneFixedPointproof · cited by 0
- Equiv.Perm.decomposeOption_symm_of_none_applystatement · cited by 0
- Equiv.Perm.decomposeOption_symm_signstatement · cited by 0