Permutations of Fin n

This file supplements Mathlib's Mathlib.GroupTheory.Perm.Fin.

Main results

• Fin.coe_cycleRange: the value of the cycle Fin.cycleRange i = (0 1 ⋯ i) at j, as a natural number, read off the comparison of the values of j and i. Unlike Fin.cycleRange_apply it needs no NeZero n instance, and both its case split and its result are stated on natural numbers, ready for omega.
• List.formPerm_finRange, Fin.formPerm_sort_univ: the cycle through the points of Fin n in increasing order is the rotation finRotate n, that is i ↦ i + 1 modulo n.
• TauCeti.isCycleOn_finRotate: the rotation finRotate n is a single cycle on all of Fin n.
• Equiv.Perm.sum_comp_symm_apply_zero: summing a function of σ⁻¹ 0 over all permutations of Fin (n + 1) counts each value n! times.

theorem Fin.coe_cycleRange {n : ℕ} (i j : Fin n) : ↑(i.cycleRange j) = if ↑j < ↑i then ↑j + 1 else if ↑j = ↑i then 0 else ↑j

The value of the cycle (0 1 ⋯ i) at j: one more than j below i, 0 at i, and j above i.

@[simp]

theorem List.formPerm_finRange (n : ℕ) : (finRange n).formPerm = finRotate n

The cycle through the points of Fin n in increasing order is the rotation i ↦ i + 1 modulo n.

@[simp]

theorem Fin.formPerm_sort_univ (n : ℕ) : (Finset.univ.sort fun (a b : Fin n) => a ≤ b).formPerm = finRotate n

The cycle through the points of Fin n, enumerated in increasing order by Finset.sort, is the rotation i ↦ i + 1 modulo n.

theorem TauCeti.isCycleOn_finRotate {n : ℕ} : (finRotate n).IsCycleOn Set.univ

The rotation i ↦ i + 1 of Fin n is a single cycle on all of Fin n.

theorem Equiv.Perm.prod_comp_symm_apply_zero {M : Type u_1} [CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) : ∏ σ : Perm (Fin (n + 1)), f ((Equiv.symm σ) 0) = (∏ p : Fin (n + 1), f p) ^ n.factorial

A product over all permutations of Fin (n + 1) of a function of σ⁻¹ 0 takes each value n! times.

theorem Equiv.Perm.sum_comp_symm_apply_zero {M : Type u_1} [AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) : ∑ σ : Perm (Fin (n + 1)), f ((Equiv.symm σ) 0) = n.factorial • ∑ p : Fin (n + 1), f p

A sum over all permutations of Fin (n + 1) of a function of σ⁻¹ 0 takes each value n! times.