isSymmetric_esymmAlgHomMonomial

Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

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

English

The polynomial esymmAlgHomMonomial(σ,t,r) is symmetric for any t and r.

Русский

Полиномиал esymmAlgHomMonomial(σ,t,r) симметричен для любых t и r.

LaTeX

$$(esymmAlgHomMonomial σ t r).IsSymmetric$$

Lean4

theorem isSymmetric_esymmAlgHomMonomial (t : Fin n →₀ ℕ) (r : R) : (esymmAlgHomMonomial σ t r).IsSymmetric :=
  (esymmAlgHom _ _ _ _).2

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

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

Разделы

Аффилиация

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