mul

Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

URI: https://scilib.ai/kg/mathlib#MvPolynomial.IsSymmetric.mul

English

If φ and ψ are symmetric, then φ × ψ is symmetric.

Русский

Если φ и ψ симметричны, то их произведение симметрично.

LaTeX

$$IsSymmetric φ → IsSymmetric ψ → IsSymmetric (φ * ψ)$$

Lean4

theorem mul (hφ : IsSymmetric φ) (hψ : IsSymmetric ψ) : IsSymmetric (φ * ψ) :=
  (symmetricSubalgebra σ R).mul_mem hφ hψ

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

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

Разделы

Аффилиация

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