eq_X_add_C_of_degree_eq_one — Mathlib

English

If deg p ≤ 1, then p = C(p.leadingCoeff) X + C(p.coeff 0).

Русский

Если deg p ≤ 1, то p = C(p.leadingCoeff) X + C(p.coeff 0).

LaTeX

$$$\deg(p)\le 1 \Rightarrow p = C(\operatorname{leadingCoeff}(p))\,X + C(p_{0}).$$$

Lean4

theorem eq_X_add_C_of_degree_eq_one (h : degree p = 1) : p = C p.leadingCoeff * X + C (p.coeff 0) :=
  (eq_X_add_C_of_degree_le_one h.le).trans
    (by rw [← Nat.cast_one] at h; rw [leadingCoeff, natDegree_eq_of_degree_eq_some h])

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