finRotate arithmetic lemmas isolated for eventual Mathlib extraction.

@[simp]

theorem finRotate_pow_apply' {m : ℕ} (hm : 0 < m) (k : ℕ) (x : Fin m) : (finRotate m ^ k) x = ⟨(↑x + k) % m, ⋯⟩

Powers of finRotate act by addition modulo m.

This is the arithmetic core behind the rotation normalization arguments.

theorem finRotate_pow_self' {m : ℕ} (hm : 0 < m) : finRotate m ^ m = 1

Rotating m times is the identity on Fin m.

theorem rotate_self_eq_zero (m : ℕ) (hm : 0 < m) (i : Fin m) : (finRotate m ^ (m - ↑i)) i = ⟨0, hm⟩

Rotating i by m - i.val lands on 0.

theorem rotate_succ_eq_one (m : ℕ) (i : Fin m) (hm2 : 2 ≤ m) : (finRotate m ^ (m - ↑i)) ((finRotate m) i) = ⟨1, ⋯⟩

Rotating finRotate m i by m - i.val lands on 1, provided m ≥ 2.