decomposeFin_symm_of_one — Mathlib

English

When the second component is the identity permutation on Fin n, the same formula holds as in the refl case: the symm equals the transposition swapping 0 and p.

Русский

Если второй компонент равен тождественной перестановке на Fin n, то та же формула как и в случае refl: symm равен транспозиции, меняющей местами 0 и p.

LaTeX

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

Lean4

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

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