The single cycle of finRotate

All points of Fin n lie on one cycle of finRotate n (Equiv.Perm.sameCycle_finRotate): for n ≥ 2 it is a cycle with full support, and for n ≤ 1 there is at most one point. So repeating w ↦ w + 1 and w ↦ w - 1 (modulo n) leads from any point to any other, which is what the slot graph of a simple graph on Fin n needs (Cslib.RotationMap.reachable_slotGraph_iff).

The values of finRotate n and of its inverse are the successor and the predecessor modulo n (val_finRotate, val_finRotate_symm), the arithmetic a machine stepping along the cycle performs.

Main results

• Equiv.Perm.sameCycle_finRotate: all points lie on the same cycle of finRotate n.
• val_finRotate, val_finRotate_symm: finRotate n and its inverse in values.

theorem val_finRotate {n : ℕ} (i : Fin n) : ↑((finRotate n) i) = if ↑i + 1 = n then 0 else ↑i + 1

The successor of finRotate, in values.

theorem val_finRotate_symm {n : ℕ} (i : Fin n) : ↑((Equiv.symm (finRotate n)) i) = if ↑i = 0 then n - 1 else ↑i - 1

The predecessor of finRotate, in values.

theorem Equiv.Perm.sameCycle_finRotate {n : ℕ} (a b : Fin n) : (finRotate n).SameCycle a b

All points of Fin n lie on the single cycle of finRotate n.