leadingCoeff_cubic — Mathlib

English

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

Русский

ведущий коэффициент кубического полинома равен a, если a ≠ 0.

LaTeX

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

Lean4

@[simp]
theorem leadingCoeff_cubic (ha : a ≠ 0) : leadingCoeff (C a * X ^ 3 + C b * X ^ 2 + C c * X + C d) = a := by
  rw [add_assoc, add_assoc, ← add_assoc (C b * X ^ 2), add_comm,
    leadingCoeff_add_of_degree_lt <| degree_quadratic_lt_degree_C_mul_X_cb ha, leadingCoeff_C_mul_X_pow]

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