map_hsymm

Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

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

English

hsymm is symmetric: IsSymmetric (hsymm σ R n).

Русский

hsymm симметричен: IsSymmetric (hsymm σ R n).

LaTeX

$$$ IsSymmetric(\\text{hsymm}(\\sigma,R,n)). $$$

Lean4

theorem map_hsymm (n : ℕ) (f : R →+* S) : map f (hsymm σ R n) = hsymm σ S n := by simp [hsymm, ← Multiset.prod_hom']

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

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

Разделы

Аффилиация

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