esymmAlgEquiv_symm_apply — Mathlib

English

With card σ = n, the inverse of esymmAlgEquiv sends the symmetric generator esymm σ R (i+1) to the polynomial X_i.

Русский

При |σ| = n обратное отображение esymmAlgEquiv отправляет симметричный образ esymm σ R (i+1) в X_i.

LaTeX

$$$(\mathrm{esymmAlgEquiv}(\sigma\, R\, hn))^{-1} \langle \mathrm{esymm}\, σ\, R (i+1), \mathrm{esymm\_isSymmetric}\ σ\, R \_\rangle = X_i$$$

Lean4

theorem esymmAlgEquiv_symm_apply (hn : Fintype.card σ = n) (i : Fin n) :
    (esymmAlgEquiv σ R hn).symm ⟨esymm σ R (i + 1), esymm_isSymmetric σ R _⟩ = X i :=
  by
  apply_fun esymmAlgHom σ R n using esymmAlgHom_injective R hn.ge
  simp_rw [esymmAlgEquiv, AlgEquiv.ofBijective_apply_symm_apply, esymmAlgHom, aeval_X]

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