hsymm_isSymmetric

Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

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

English

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

Русский

hsymm симметричен (альтернативное утверждение): IsSymmetric (hsymm σ R n).

LaTeX

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

Lean4

theorem hsymm_isSymmetric (n : ℕ) : IsSymmetric (hsymm σ R n) :=
  rename_hsymm _ _ n

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

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

Разделы

Аффилиация

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