add

Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

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

English

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

Русский

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

LaTeX

$$IsSymmetric φ → IsSymmetric ψ → IsSymmetric (φ + ψ)$$

Lean4

theorem add (hφ : IsSymmetric φ) (hψ : IsSymmetric ψ) : IsSymmetric (φ + ψ) :=
  (symmetricSubalgebra σ R).add_mem hφ hψ

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

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

Разделы

Аффилиация

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