sub

Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

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

English

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

Русский

Если φ и ψ симметричны, то φ − ψ симметричен.

LaTeX

$$IsSymmetric φ → IsSymmetric ψ → IsSymmetric (φ - ψ)$$

Lean4

theorem sub (hφ : IsSymmetric φ) (hψ : IsSymmetric ψ) : IsSymmetric (φ - ψ) :=
  (symmetricSubalgebra σ R).sub_mem hφ hψ

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

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

Разделы

Аффилиация

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