# Results on polynomials of specific small degrees #

source
theorem Polynomial.eq_X_add_C_of_degree_le_one {R : Type u} [Semiring R] {p : Polynomial R} (h : p.degree ≤ 1) :
p = C (p.coeff 1) * X + C (p.coeff 0)
source
theorem Polynomial.eq_X_add_C_of_degree_eq_one {R : Type u} [Semiring R] {p : Polynomial R} (h : p.degree = 1) :
p = C p.leadingCoeff * X + C (p.coeff 0)
source
theorem Polynomial.eq_X_add_C_of_natDegree_le_one {R : Type u} [Semiring R] {p : Polynomial R} (h : p.natDegree ≤ 1) :
p = C (p.coeff 1) * X + C (p.coeff 0)
source
theorem Polynomial.Monic.eq_X_add_C {R : Type u} [Semiring R] {p : Polynomial R} (hm : p.Monic) (hnd : p.natDegree = 1) :
p = X + C (p.coeff 0)
source
theorem Polynomial.exists_eq_X_add_C_of_natDegree_le_one {R : Type u} [Semiring R] {p : Polynomial R} (h : p.natDegree ≤ 1) :
∃ (a : R) (b : R), p = C a * X + C b
source
theorem Polynomial.zero_le_degree_iff {R : Type u} [Semiring R] {p : Polynomial R} :
0 ≤ p.degree ↔ p ≠ 0
source
theorem Polynomial.ne_zero_of_coe_le_degree {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (hdeg : ↑n ≤ p.degree) :
p ≠ 0
source
theorem Polynomial.le_natDegree_of_coe_le_degree {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (hdeg : ↑n ≤ p.degree) :
n ≤ p.natDegree
source
theorem Polynomial.degree_linear_le {R : Type u} {a b : R} [Semiring R] :
(C a * X + C b).degree ≤ 1
source
theorem Polynomial.degree_linear_lt {R : Type u} {a b : R} [Semiring R] :
(C a * X + C b).degree < 2
source
@[simp]
theorem Polynomial.degree_linear {R : Type u} {a b : R} [Semiring R] (ha : a ≠ 0) :
(C a * X + C b).degree = 1
source
theorem Polynomial.natDegree_linear_le {R : Type u} {a b : R} [Semiring R] :
(C a * X + C b).natDegree ≤ 1
source
theorem Polynomial.natDegree_linear {R : Type u} {a b : R} [Semiring R] (ha : a ≠ 0) :
(C a * X + C b).natDegree = 1
source
@[simp]
theorem Polynomial.leadingCoeff_linear {R : Type u} {a b : R} [Semiring R] (ha : a ≠ 0) :
(C a * X + C b).leadingCoeff = a
source
theorem Polynomial.degree_quadratic_le {R : Type u} {a b c : R} [Semiring R] :
(C a * X ^ 2 + C b * X + C c).degree ≤ 2
source
theorem Polynomial.degree_quadratic_lt {R : Type u} {a b c : R} [Semiring R] :
(C a * X ^ 2 + C b * X + C c).degree < 3
source
theorem Polynomial.degree_linear_lt_degree_C_mul_X_sq {R : Type u} {a b c : R} [Semiring R] (ha : a ≠ 0) :
(C b * X + C c).degree < (C a * X ^ 2).degree
source
@[simp]
theorem Polynomial.degree_quadratic {R : Type u} {a b c : R} [Semiring R] (ha : a ≠ 0) :
(C a * X ^ 2 + C b * X + C c).degree = 2
source
theorem Polynomial.natDegree_quadratic_le {R : Type u} {a b c : R} [Semiring R] :
(C a * X ^ 2 + C b * X + C c).natDegree ≤ 2
source
theorem Polynomial.natDegree_quadratic {R : Type u} {a b c : R} [Semiring R] (ha : a ≠ 0) :
(C a * X ^ 2 + C b * X + C c).natDegree = 2
source
@[simp]
theorem Polynomial.leadingCoeff_quadratic {R : Type u} {a b c : R} [Semiring R] (ha : a ≠ 0) :
(C a * X ^ 2 + C b * X + C c).leadingCoeff = a
source
theorem Polynomial.degree_cubic_le {R : Type u} {a b c d : R} [Semiring R] :
(C a * X ^ 3 + C b * X ^ 2 + C c * X + C d).degree ≤ 3
source
theorem Polynomial.degree_cubic_lt {R : Type u} {a b c d : R} [Semiring R] :
(C a * X ^ 3 + C b * X ^ 2 + C c * X + C d).degree < 4
source
theorem Polynomial.degree_quadratic_lt_degree_C_mul_X_cb {R : Type u} {a b c d : R} [Semiring R] (ha : a ≠ 0) :
(C b * X ^ 2 + C c * X + C d).degree < (C a * X ^ 3).degree
source
@[simp]
theorem Polynomial.degree_cubic {R : Type u} {a b c d : R} [Semiring R] (ha : a ≠ 0) :
(C a * X ^ 3 + C b * X ^ 2 + C c * X + C d).degree = 3
source
theorem Polynomial.natDegree_cubic_le {R : Type u} {a b c d : R} [Semiring R] :
(C a * X ^ 3 + C b * X ^ 2 + C c * X + C d).natDegree ≤ 3
source
theorem Polynomial.natDegree_cubic {R : Type u} {a b c d : R} [Semiring R] (ha : a ≠ 0) :
(C a * X ^ 3 + C b * X ^ 2 + C c * X + C d).natDegree = 3
source
@[simp]
theorem Polynomial.leadingCoeff_cubic {R : Type u} {a b c d : R} [Semiring R] (ha : a ≠ 0) :
(C a * X ^ 3 + C b * X ^ 2 + C c * X + C d).leadingCoeff = a