degree_cubic — Mathlib

English

For a ≠ 0, deg(C(a)·X^3 + C(b)·X^2 + C(c)·X + C(d)) = 3.

Русский

Для a ≠ 0 степени кубического полинома равна 3.

LaTeX

$$(a \neq 0) \Rightarrow \deg(C(a)\,X^3 + C(b)\,X^2 + C(c)\,X + C(d)) = 3$$

Lean4

@[simp]
theorem degree_cubic (ha : a ≠ 0) : degree (C a * X ^ 3 + C b * X ^ 2 + C c * X + C d) = 3 :=
  by
  rw [add_assoc, add_assoc, ← add_assoc (C b * X ^ 2),
    degree_add_eq_left_of_degree_lt <| degree_quadratic_lt_degree_C_mul_X_cb ha, degree_C_mul_X_pow 3 ha]
  rfl

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