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.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