Theorems · Theorem · group theory
cycleType_finRotate
∀ {n : ℕ}, (finRotate (n + 2)).cycleType = {n + 2}- Defined in
- Mathlib.GroupTheory.Perm.Fin
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetproof · cited by 13,712
- Multisetstatement and proof · cited by 2,627
- Finset.cardproof · cited by 2,327
- Fintype.card_finproof · cited by 270
- Equiv.Perm.cycleTypestatement · cited by 87
- finRotatestatement · cited by 36
- Equiv.Perm.IsCycle.cycleTypeproof · cited by 12
- isCycle_finRotateproof · cited by 3
- support_finRotateproof · cited by 2
Cited by2
Results whose statement or proof uses this declaration.
- Fin.cycleType_cycleRangeproof · cited by 2
- cycleType_finRotate_of_leproof · cited by 0