English
Permutations of Fin(n+1) are in bijection with a fixed element and a permutation of Fin n, via a decomposition map splitting off the last element.
Русский
Перестановки на Fin(n+1) эквивалентны фиксации одного элемента и перестановке остальных на Fin n.
LaTeX
$$$\mathrm{decomposeFin} : \mathrm{Perm}(\mathrm{Fin}\, (n+1)) \simeq (\mathrm{Fin}\, (n+1)) \times \mathrm{Perm}(\mathrm{Fin}\, n)$$$
Lean4
/-- Permutations of `Fin (n + 1)` are equivalent to fixing a single
`Fin (n + 1)` and permuting the remaining with a `Perm (Fin n)`.
The fixed `Fin (n + 1)` is swapped with `0`. -/
def decomposeFin {n : ℕ} : Perm (Fin n.succ) ≃ Fin n.succ × Perm (Fin n) :=
((Equiv.permCongr <| finSuccEquiv n).trans Equiv.Perm.decomposeOption).trans
(Equiv.prodCongr (finSuccEquiv n).symm (Equiv.refl _))
