degree_cubic_le — Mathlib

English

Let a ≠ 0. Then deg(C(a)·X^3 + C(b)·X^2 + C(c)·X + C(d)) ≤ 3.

Русский

Пусть a ≠ 0. Тогда deg(C(a)·X^3 + C(b)·X^2 + C(c)·X + C(d)) ≤ 3.

LaTeX

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

Lean4

theorem degree_cubic_le : degree (C a * X ^ 3 + C b * X ^ 2 + C c * X + C d) ≤ 3 := by
  simpa only [add_assoc] using
    degree_add_le_of_degree_le (degree_C_mul_X_pow_le 3 a)
      (le_trans degree_quadratic_le <| WithBot.coe_le_coe.mpr <| Nat.le_succ 2)

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