Permutations as lists

A permutation of Fin n can be written in one-line notation as a list containing every element of Fin n exactly once. This file packages that correspondence as an equivalence.

noncomputable def TauCeti.permutationWordEquiv (n : ℕ) : Equiv.Perm (Fin n) ≃ { w : List (Fin n) // w.Perm (List.finRange n) }

Permutations of Fin n correspond to lists containing every element of Fin n exactly once, by writing a permutation in one-line notation.

@[simp]

theorem TauCeti.permutationWordEquiv_apply_coe (n : ℕ) (σ : Equiv.Perm (Fin n)) : ↑((permutationWordEquiv n) σ) = List.ofFn ⇑σ

The forward permutation-to-word equivalence is List.ofFn.