Theorems · Definition · combinatorics
finRotate
(n : ℕ) → Equiv.Perm (Fin n)
Rotate Fin n one step to the right.
- Defined in
- Mathlib.Logic.Equiv.Fin.Rotate
- Cited by
- 36 results in Mathlib
- Foundations
- Depth 29 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Equiv.Permstatement and proof · cited by 1,375
- Equiv.transproof · cited by 337
- Equiv.reflproof · cited by 274
- finCongrproof · cited by 78
- finAddFlipproof · cited by 5
Cited by40
Results whose statement or proof uses this declaration.
- Fin.cycleRangeproof · cited by 35
- finRotate_applystatement and proof · cited by 12
- Fin.cycleRange_of_gtproof · cited by 6
- Fin.sign_cycleRangeproof · cited by 4
- linearIndependent_finSnocproof · cited by 3
- isCycle_finRotatestatement and proof · cited by 3
- Fin.cycleRange_of_leproof · cited by 3
- finRotate_onestatement and proof · cited by 3
- Fin.snoc_eq_cons_rotatestatement · cited by 3
- cycleType_finRotatestatement · cited by 2
- coe_finRotatestatement · cited by 2
- sign_finRotatestatement and proof · cited by 2