Documentation

Mathlib.Algebra.Polynomial.Degree.SmallDegree

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 = Polynomial.C (p.coeff 1) * Polynomial.X + Polynomial.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 = Polynomial.C p.leadingCoeff * Polynomial.X + Polynomial.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 = Polynomial.C (p.coeff 1) * Polynomial.X + Polynomial.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 = Polynomial.X + Polynomial.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 = Polynomial.C a * Polynomial.X + Polynomial.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] :
(Polynomial.C a * Polynomial.X + Polynomial.C b).degree ≤ 1
source
theorem Polynomial.degree_linear_lt {R : Type u} {a b : R} [Semiring R] :
(Polynomial.C a * Polynomial.X + Polynomial.C b).degree < 2
source
@[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
source
theorem Polynomial.natDegree_linear_le {R : Type u} {a b : R} [Semiring R] :
(Polynomial.C a * Polynomial.X + Polynomial.C b).natDegree ≤ 1
source
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
source
@[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
source
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
source
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
source
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
source
@[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
source
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
source
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
source
@[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
source
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
source
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
source
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
source
@[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
source
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
source
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
source
@[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