Degree of univariate polynomials #
Main definitions #
Polynomial.degree
: the degree of a polynomial, where0
has degree⊥
Polynomial.natDegree
: the degree of a polynomial, where0
has degree0
Polynomial.leadingCoeff
: the leading coefficient of a polynomialPolynomial.Monic
: a polynomial is monic if its leading coefficient is 0Polynomial.nextCoeff
: the next coefficient after the leading coefficient
Main results #
Polynomial.degree_eq_natDegree
: the degree and natDegree coincide for nonzero polynomials
leadingCoeff p
gives the coefficient of the highest power of X
in p
Instances For
a polynomial is Monic
if its leading coefficient is 1
Instances For
Equations
@[simp]
theorem
Polynomial.Monic.coeff_natDegree
{R : Type u}
[Semiring R]
{p : Polynomial R}
(hp : p.Monic)
:
@[simp]
theorem
Polynomial.degree_eq_iff_natDegree_eq
{R : Type u}
[Semiring R]
{p : Polynomial R}
{n : ℕ}
(hp : p ≠ 0)
:
theorem
Polynomial.degree_eq_iff_natDegree_eq_of_pos
{R : Type u}
[Semiring R]
{p : Polynomial R}
{n : ℕ}
(hn : 0 < n)
:
theorem
Polynomial.natDegree_eq_of_degree_eq_some
{R : Type u}
[Semiring R]
{p : Polynomial R}
{n : ℕ}
(h : p.degree = ↑n)
:
@[simp]
theorem
Polynomial.natDegree_eq_of_degree_eq
{R : Type u}
{S : Type v}
[Semiring R]
{p : Polynomial R}
[Semiring S]
{q : Polynomial S}
(h : p.degree = q.degree)
:
theorem
Polynomial.degree_le_degree
{R : Type u}
[Semiring R]
{p q : Polynomial R}
(h : q.coeff p.natDegree ≠ 0)
:
theorem
Polynomial.natDegree_le_iff_degree_le
{R : Type u}
[Semiring R]
{p : Polynomial R}
{n : ℕ}
:
theorem
Polynomial.natDegree_lt_iff_degree_lt
{R : Type u}
{n : ℕ}
[Semiring R]
{p : Polynomial R}
(hp : p ≠ 0)
:
Alias of the forward direction of Polynomial.natDegree_le_iff_degree_le
.
Alias of the reverse direction of Polynomial.natDegree_le_iff_degree_le
.
theorem
Polynomial.natDegree_le_natDegree
{R : Type u}
{S : Type v}
[Semiring R]
{p : Polynomial R}
[Semiring S]
{q : Polynomial S}
(hpq : p.degree ≤ q.degree)
:
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
Polynomial.natDegree_neg_le_of_le
{R : Type u}
{m : ℕ}
[Ring R]
{p : Polynomial R}
(hp : p.natDegree ≤ m)
:
@[simp]
@[simp]
The second-highest coefficient, or 0 for constants
Instances For
@[simp]
theorem
Polynomial.nextCoeff_of_natDegree_pos
{R : Type u}
[Semiring R]
{p : Polynomial R}
(hp : 0 < p.natDegree)
:
theorem
Polynomial.natDegree_add_le_of_degree_le
{R : Type u}
[Semiring R]
{p q : Polynomial R}
{n : ℕ}
(hp : p.natDegree ≤ n)
(hq : q.natDegree ≤ n)
:
theorem
Polynomial.natDegree_add_le_of_le
{R : Type u}
{n m : ℕ}
[Semiring R]
{p q : Polynomial R}
(hp : p.natDegree ≤ m)
(hq : q.natDegree ≤ n)
:
@[simp]
theorem
Polynomial.degree_sum_le
{R : Type u}
[Semiring R]
{ι : Type u_1}
(s : Finset ι)
(f : ι → Polynomial R)
:
@[simp]
@[simp]
theorem
Polynomial.Monic.ne_zero
{R : Type u_2}
[Semiring R]
[Nontrivial R]
{p : Polynomial R}
(hp : p.Monic)
:
theorem
Polynomial.Monic.ne_zero_of_ne
{R : Type u}
[Semiring R]
(h : 0 ≠ 1)
{p : Polynomial R}
(hp : p.Monic)
:
theorem
Polynomial.Monic.ne_zero_of_polynomial_ne
{R : Type u}
[Semiring R]
{p q r : Polynomial R}
(hp : p.Monic)
(hne : q ≠ r)
:
theorem
Polynomial.natDegree_mul_le_of_le
{R : Type u}
{n m : ℕ}
[Semiring R]
{p q : Polynomial R}
(hp : p.natDegree ≤ m)
(hg : q.natDegree ≤ n)
:
theorem
Polynomial.natDegree_sub_le_of_le
{R : Type u}
{n m : ℕ}
[Ring R]
{p q : Polynomial R}
(hp : p.natDegree ≤ m)
(hq : q.natDegree ≤ n)
:
theorem
Polynomial.degree_sub_lt
{R : Type u}
[Ring R]
{p q : Polynomial R}
(hd : p.degree = q.degree)
(hp0 : p ≠ 0)
(hlc : p.leadingCoeff = q.leadingCoeff)
: