eq_quadratic_of_degree_le_two — Mathlib

English

If a polynomial p over a semiring has degree at most 2, then p can be written as p = a X^2 + b X + c with a = p.coeff 2, b = p.coeff 1, c = p.coeff 0.

Русский

Если p над полукольцом имеет deg p ≤ 2, то p = a X^2 + b X + c, где a = coeff 2, b = coeff 1, c = coeff 0.

LaTeX

$$$\\forall R [\\mathrm{Semiring}\\ R]\\; {p \\in R[X]},\\; p.d\\mathrm{egree} \\le 2 \\Rightarrow p = C(p.\\mathrm{coeff}\\,2) \\cdot X^2 + C(p.\\mathrm{coeff}\\,1) \\cdot X + C(p.\\mathrm{coeff}\\,0)$$$

Lean4

theorem eq_quadratic_of_degree_le_two [Semiring R] {p : R[X]} (hp : p.degree ≤ 2) :
    p = C (p.coeff 2) * X ^ 2 + C (p.coeff 1) * X + C (p.coeff 0) :=
  by
  rw [p.as_sum_range_C_mul_X_pow' (Nat.lt_of_le_of_lt (natDegree_le_iff_degree_le.mpr hp) (Nat.lt_add_one 2))]
  simp [Finset.sum_range_succ]
  abel

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