totalDegree_mul

Mathlib.Algebra.MvPolynomial.Degrees

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

← MathLib Explorer

English

For a monomial s, the degree is bounded by the coordinates of s.

Русский

Степень монома ограничена координатами векторa s.

LaTeX

$$$\deg_i(\mathrm{monomial}\, s) = s(i)$$$

Lean4

theorem totalDegree_mul (a b : MvPolynomial σ R) : (a * b).totalDegree ≤ a.totalDegree + b.totalDegree :=
  sup_support_mul_le (by exact (Finsupp.sum_add_index' (fun _ => rfl) (fun _ _ _ => rfl)).le) _ _

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

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

Разделы

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

Аффилиация

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