eq_X_add_C_of_degree_le_one — Mathlib

English

If a polynomial p has degree at most 1, then p can be written as p = C(p1)·X + C(p0), where p1 = coeff 1 and p0 = coeff 0.

Русский

Если степень полинома p не больше 1, то p можно записать в виде p = C(p1)·X + C(p0), где p1 = coef 1, p0 = coef 0.

LaTeX

$$$\deg(p) \le 1 \;\Rightarrow\; p = C(p_1) \cdot X + C(p_0)$$$

Lean4

theorem eq_X_add_C_of_degree_le_one (h : degree p ≤ 1) : p = C (p.coeff 1) * X + C (p.coeff 0) :=
  ext fun n =>
    Nat.casesOn n (by simp) fun n =>
      Nat.casesOn n (by simp [coeff_C]) fun m =>
        by
        have : degree p < m.succ.succ := lt_of_le_of_lt h Nat.one_lt_ofNat
        simp [coeff_eq_zero_of_degree_lt this]

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