Results on polynomials of specific small degrees

theorem Polynomial.eq_X_add_C_of_degree_le_one {R : Type u} [Semiring R] {p : Polynomial R} (h : p.degree ≤ 1) : p = Polynomial.C (p.coeff 1) * Polynomial.X + Polynomial.C (p.coeff 0)

theorem Polynomial.eq_X_add_C_of_degree_eq_one {R : Type u} [Semiring R] {p : Polynomial R} (h : p.degree = 1) : p = Polynomial.C p.leadingCoeff * Polynomial.X + Polynomial.C (p.coeff 0)

theorem Polynomial.eq_X_add_C_of_natDegree_le_one {R : Type u} [Semiring R] {p : Polynomial R} (h : p.natDegree ≤ 1) : p = Polynomial.C (p.coeff 1) * Polynomial.X + Polynomial.C (p.coeff 0)

theorem Polynomial.Monic.eq_X_add_C {R : Type u} [Semiring R] {p : Polynomial R} (hm : p.Monic) (hnd : p.natDegree = 1) : p = Polynomial.X + Polynomial.C (p.coeff 0)

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 = Polynomial.C a * Polynomial.X + Polynomial.C b

theorem Polynomial.zero_le_degree_iff {R : Type u} [Semiring R] {p : Polynomial R} : 0 ≤ p.degree ↔ p ≠ 0

theorem Polynomial.ne_zero_of_coe_le_degree {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (hdeg : ↑n ≤ p.degree) : p ≠ 0

theorem Polynomial.le_natDegree_of_coe_le_degree {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (hdeg : ↑n ≤ p.degree) : n ≤ p.natDegree

theorem Polynomial.degree_linear_le {R : Type u} {a b : R} [Semiring R] : (Polynomial.C a * Polynomial.X + Polynomial.C b).degree ≤ 1

theorem Polynomial.degree_linear_lt {R : Type u} {a b : R} [Semiring R] : (Polynomial.C a * Polynomial.X + Polynomial.C b).degree < 2

@[simp]

theorem Polynomial.degree_linear {R : Type u} {a b : R} [Semiring R] (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X + Polynomial.C b).degree = 1

theorem Polynomial.natDegree_linear_le {R : Type u} {a b : R} [Semiring R] : (Polynomial.C a * Polynomial.X + Polynomial.C b).natDegree ≤ 1

theorem Polynomial.natDegree_linear {R : Type u} {a b : R} [Semiring R] (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X + Polynomial.C b).natDegree = 1

@[simp]

theorem Polynomial.leadingCoeff_linear {R : Type u} {a b : R} [Semiring R] (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X + Polynomial.C b).leadingCoeff = a

theorem Polynomial.degree_quadratic_le {R : Type u} {a b c : R} [Semiring R] : (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).degree ≤ 2

theorem Polynomial.degree_quadratic_lt {R : Type u} {a b c : R} [Semiring R] : (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).degree < 3

theorem Polynomial.degree_linear_lt_degree_C_mul_X_sq {R : Type u} {a b c : R} [Semiring R] (ha : a ≠ 0) : (Polynomial.C b * Polynomial.X + Polynomial.C c).degree < (Polynomial.C a * Polynomial.X ^ 2).degree

@[simp]

theorem Polynomial.degree_quadratic {R : Type u} {a b c : R} [Semiring R] (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).degree = 2

theorem Polynomial.natDegree_quadratic_le {R : Type u} {a b c : R} [Semiring R] : (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).natDegree ≤ 2

theorem Polynomial.natDegree_quadratic {R : Type u} {a b c : R} [Semiring R] (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).natDegree = 2

@[simp]

theorem Polynomial.leadingCoeff_quadratic {R : Type u} {a b c : R} [Semiring R] (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).leadingCoeff = a

theorem Polynomial.degree_cubic_le {R : Type u} {a b c d : R} [Semiring R] : (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).degree ≤ 3

theorem Polynomial.degree_cubic_lt {R : Type u} {a b c d : R} [Semiring R] : (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).degree < 4

theorem Polynomial.degree_quadratic_lt_degree_C_mul_X_cb {R : Type u} {a b c d : R} [Semiring R] (ha : a ≠ 0) : (Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).degree < (Polynomial.C a * Polynomial.X ^ 3).degree

@[simp]

theorem Polynomial.degree_cubic {R : Type u} {a b c d : R} [Semiring R] (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).degree = 3

theorem Polynomial.natDegree_cubic_le {R : Type u} {a b c d : R} [Semiring R] : (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).natDegree ≤ 3

theorem Polynomial.natDegree_cubic {R : Type u} {a b c d : R} [Semiring R] (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).natDegree = 3

@[simp]

theorem Polynomial.leadingCoeff_cubic {R : Type u} {a b c d : R} [Semiring R] (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).leadingCoeff = a