esymmAlgHomMonomial

Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

URI: https://scilib.ai/kg/mathlib#MvPolynomial.esymmAlgHomMonomial

← MathLib Explorer

English

msymm(μ) is symmetric for any partition μ.

Русский

msymm(μ) симметричен для любого μ.

LaTeX

$$IsSymmetric( msymm_{\\sigma,R}(\\mu) )$$

Lean4

/-- The image of a monomial under `esymmAlgHom`. -/
noncomputable def esymmAlgHomMonomial (t : Fin n →₀ ℕ) (r : R) : MvPolynomial σ R :=
  (esymmAlgHom σ R n <| monomial t r).val

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru