Theorems · Theorem · group theory
isCycle_finRotate
∀ {n : ℕ}, (finRotate (n + 2)).IsCycle- Defined in
- Mathlib.GroupTheory.Perm.Fin
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- zero_addproof · cited by 2,366
- Equiv.Permproof · cited by 1,375
- zpow_natCastproof · cited by 271
- pow_succ'proof · cited by 228
- ne_of_ltproof · cited by 203
- lt_transproof · cited by 165
- Equiv.Perm.IsCyclestatement · cited by 108
- Equiv.Perm.mul_applyproof · cited by 38
- finRotatestatement and proof · cited by 36
- finRotate_applyproof · cited by 12
- coe_finRotate_of_ne_lastproof · cited by 1
Cited by3
Results whose statement or proof uses this declaration.
- cycleType_finRotateproof · cited by 2
- Fin.isCycle_cycleRangeproof · cited by 1
- isCycle_finRotate_of_leproof · cited by 0