esymmAlgHom — Mathlib

English

msymm(Indiscrete 0) = 1.

Русский

msymm(Indiscrete 0) = 1.

LaTeX

$$$\\mathrm{msymm}_{\\sigma,R}(\\mathrm{Nat.Partition.indiscrete}(0)) = 1$$$

Lean4

/-- The `R`-algebra homomorphism from $R[x_1,\dots,x_n]$ to the symmetric subalgebra of
  $R[\{x_i \mid i ∈ σ\}]$ sending $x_i$ to the $i$-th elementary symmetric polynomial. -/
noncomputable def esymmAlgHom : MvPolynomial (Fin n) R →ₐ[R] symmetricSubalgebra σ R :=
  aeval (fun i ↦ ⟨esymm σ R (i + 1), esymm_isSymmetric σ R _⟩)

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