decomposeFin_symm_of_refl — Mathlib

English

Let p be a element of Fin(n+1). The inverse of the standard decomposition of Fin sends (p, id) to the transposition swapping 0 and p on Fin(n+1).

Русский

Пусть p принадлежит Fin(n+1). Обратимое разложение Fin отправляет (p, идентично на Fin n) в транспозицию, меняющую местами 0 и p на Fin(n+1).

LaTeX

$$$ \\mathrm{decomposeFin.symm}(p, \\mathrm{id}) = \\mathrm{swap}(0, p)$$$

Lean4

@[simp]
theorem decomposeFin_symm_of_refl {n : ℕ} (p : Fin (n + 1)) :
    Equiv.Perm.decomposeFin.symm (p, Equiv.refl _) = swap 0 p := by simp [Equiv.Perm.decomposeFin, Equiv.permCongr_def]

Похожие утверждения