totalDegree_smul_le

Mathlib.Algebra.MvPolynomial.Degrees

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

← MathLib Explorer

English

DegreeOf equals the supremum over supports; use a concrete f to illustrate.

Русский

DegreeOf равен верхней грани по опоре; приведём конкретный пример.

LaTeX

$$$\deg_n(f) = \sup_{m \in \operatorname{support}(f)} m(n)$$$

Lean4

theorem totalDegree_smul_le [CommSemiring S] [DistribMulAction R S] (a : R) (f : MvPolynomial σ S) :
    (a • f).totalDegree ≤ f.totalDegree :=
  Finset.sup_mono support_smul

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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