le_trailingDegree_C

Mathlib.Algebra.Polynomial.Degree.TrailingDegree

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

English

For any a, the trailing-degree of the constant polynomial C a is nonnegative: 0 ≤ trailingDegree(C a).

Русский

Для любого a трайлDegree константного полинома C a неотрицательно: 0 ≤ trailingDegree(C a).

LaTeX

$$$0 \le \operatorname{trailingDegree}(C a)$$$

Lean4

theorem le_trailingDegree_C : (0 : ℕ∞) ≤ trailingDegree (C a) :=
  le_trailingDegree_monomial

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

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

Разделы

Аффилиация

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