supDegree_eq_degree

Mathlib.Algebra.Polynomial.Degree.Operations

URI: https://scilib.ai/kg/mathlib#Polynomial.supDegree_eq_degree

English

The supremum of the indices with nonzero coefficients equals the degree of the polynomial

Русский

Наибольший индекс, при котором коэффициент не равен нулю, равен степени многочлена.

LaTeX

$$$\\sup\\{n \\in \\mathbb{N} \\mid p_n \\neq 0\\} = \\operatorname{degree}(p)$$$

Lean4

theorem supDegree_eq_degree (p : R[X]) : p.toFinsupp.supDegree WithBot.some = p.degree :=
  max_eq_sup_coe

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

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

Разделы

Аффилиация

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