Cyclic permutations on Fin n

This file defines

• finRotate, which corresponds to the cycle (1, ..., n) on Fin n
• finCycle, the permutation that adds a fixed number to each element of Fin n and proves various lemmas about them.

def finRotate (n : ℕ) : Equiv.Perm (Fin n)

Rotate Fin n one step to the right.

@[simp]

theorem finRotate_zero : finRotate 0 = Equiv.refl (Fin 0)

theorem finRotate_succ (n : ℕ) : finRotate (n + 1) = finAddFlip.trans (finCongr ⋯)

theorem finRotate_of_lt {n k : ℕ} (h : k < n) : (finRotate (n + 1)) ⟨k, ⋯⟩ = ⟨k + 1, ⋯⟩

theorem finRotate_last' {n : ℕ} : (finRotate (n + 1)) ⟨n, ⋯⟩ = ⟨0, ⋯⟩

theorem finRotate_last {n : ℕ} : (finRotate (n + 1)) (Fin.last n) = 0

theorem Fin.snoc_eq_cons_rotate {n : ℕ} {α : Type u_1} (v : Fin n → α) (a : α) : snoc v a = fun (i : Fin (n + 1)) => cons a v ((finRotate (n + 1)) i)

@[simp]

theorem finRotate_one : finRotate 1 = Equiv.refl (Fin 1)

@[simp]

theorem finRotate_apply {n : ℕ} (i : Fin n) : (finRotate n) i = i + 1

@[deprecated finRotate_apply (since := "2026-03-29")]

theorem finRotate_succ_apply {n : ℕ} (i : Fin (n + 1)) : (finRotate (n + 1)) i = i + 1

theorem finRotate_apply_zero {n : ℕ} : (finRotate n.succ) 0 = 1

theorem coe_finRotate_of_ne_last {n : ℕ} {i : Fin n.succ} (h : i ≠ Fin.last n) : ↑((finRotate (n + 1)) i) = ↑i + 1

theorem coe_finRotate {n : ℕ} (i : Fin n.succ) : ↑((finRotate n.succ) i) = if i = Fin.last n then 0 else ↑i + 1

theorem lt_finRotate_iff_ne_last {n : ℕ} (i : Fin (n + 1)) : i < (finRotate (n + 1)) i ↔ i ≠ Fin.last n

theorem lt_finRotate_iff_ne_neg_one {n : ℕ} [NeZero n] (i : Fin n) : i < (finRotate n) i ↔ i ≠ -1

@[simp]

theorem finRotate_symm_apply {n : ℕ} (i : Fin n) : (Equiv.symm (finRotate n)) i = i - 1

@[deprecated finRotate_symm_apply (since := "2026-03-29")]

theorem finRotate_succ_symm_apply {n : ℕ} [NeZero n] (i : Fin n) : (Equiv.symm (finRotate n)) i = i - 1

theorem coe_finRotate_symm_of_ne_zero {n : ℕ} [NeZero n] {i : Fin n} (hi : i ≠ 0) : ↑((Equiv.symm (finRotate n)) i) = ↑i - 1

theorem finRotate_symm_lt_iff_ne_zero {n : ℕ} [NeZero n] (i : Fin n) : (Equiv.symm (finRotate n)) i < i ↔ i ≠ 0

def finCycle {n : ℕ} (k : Fin n) : Equiv.Perm (Fin n)

The permutation on Fin n that adds k to each number.

@[simp]

theorem finCycle_apply {n : ℕ} (k i : Fin n) : (finCycle k) i = i + k

@[simp]

theorem finCycle_symm_apply {n : ℕ} (k i : Fin n) : (Equiv.symm (finCycle k)) i = i - k

theorem finCycle_eq_finRotate_iterate {n : ℕ} {k : Fin n} : ⇑(finCycle k) = (⇑(finRotate n))^[↑k]