natDegree_of_a_ne_zero'

Mathlib.Algebra.CubicDiscriminant

URI: https://scilib.ai/kg/mathlib#Cubic.natDegree_of_a_ne_zero'

English

If a ≠ 0, then the polynomial has natDegree 3.

Русский

Если a ≠ 0, то натуральная степень полинома равна 3.

LaTeX

$$$a \\neq 0 \\Rightarrow (P.toPoly).natDegree = 3$$$

Lean4

theorem natDegree_of_a_ne_zero' (ha : a ≠ 0) : (toPoly ⟨a, b, c, d⟩).natDegree = 3 := by simp [ha]

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

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

Разделы

Аффилиация

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