leadingCoeff_quadratic — Mathlib

English

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

Русский

ведущий коэффициент квадратичного полинома C(a)·X^2 + C(b)·X + C(c) равен a, если a ≠ 0.

LaTeX

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

Lean4

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

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