natDegree_cubic

Mathlib.Algebra.Polynomial.Degree.SmallDegree

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

← MathLib Explorer

English

natDegree(C(a)·X^3 + C(b)·X^2 + C(c)·X + C(d)) = 3 when a ≠ 0.

Русский

natDegree(C(a)·X^3 + C(b)·X^2 + C(c)·X + C(d)) = 3, если a ≠ 0.

LaTeX

$$(a \neq 0) \Rightarrow \operatorname{natDegree}(C(a)\,X^3 + C(b)\,X^2 + C(c)\,X + C(d)) = 3$$

Lean4

theorem natDegree_cubic (ha : a ≠ 0) : natDegree (C a * X ^ 3 + C b * X ^ 2 + C c * X + C d) = 3 :=
  natDegree_eq_of_degree_eq_some <| degree_cubic ha

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

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

Разделы

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

Аффилиация

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