exists_eq_X_add_C_of_natDegree_le_one

English

Let p be a polynomial over a semiring R with natDegree(p) ≤ 1. Then there exist a,b in R such that p = C(a)·X + C(b). In words, a polynomial of degree at most 1 is linear and has the form p(x) = a x + b.

Русский

Пусть p является полиномом над полем/кольцом R с natDegree(p) ≤ 1. Тогда существуют a,b ∈ R такие, что p = C(a)·X + C(b). Другими словами, полином степени не более 1 имеет вид p(x) = a x + b.

LaTeX

$$$\forall p \in R[X],\ \operatorname{natDegree}(p) \le 1 \Rightarrow \exists a,b \in R:\ p = C(a) \cdot X + C(b)$$$

Lean4

theorem exists_eq_X_add_C_of_natDegree_le_one (h : natDegree p ≤ 1) : ∃ a b, p = C a * X + C b :=
  ⟨p.coeff 1, p.coeff 0, eq_X_add_C_of_natDegree_le_one h⟩

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