Trailing degree of univariate polynomials #
Main definitions #
trailing_degree p
: the multiplicity ofX
in the polynomialp
nat_trailing_degree
: a variant oftrailing_degree
that takes values in the natural numberstrailing_coeff
: the coefficient at indexnat_trailing_degree p
Converts most results about degree
, nat_degree
and leading_coeff
to results about the bottom
end of a polynomial
trailing_degree p
is the multiplicity of x
in the polynomial p
, i.e. the smallest
X
-exponent in p
.
trailing_degree p = some n
when p ≠ 0
and n
is the smallest power of X
that appears
in p
, otherwise
trailing_degree 0 = ⊤
.
Equations
theorem
polynomial.trailing_degree_lt_wf
{R : Type u}
[semiring R] :
well_founded (λ (p q : polynomial R), p.trailing_degree < q.trailing_degree)
nat_trailing_degree p
forces trailing_degree p
to ℕ
, by defining
nat_trailing_degree ⊤ = 0
.
Equations
trailing_coeff p
gives the coefficient of the smallest power of X
in p
Equations
a polynomial is monic_at
if its trailing coefficient is 1
Equations
- p.trailing_monic = (p.trailing_coeff = 1)
Instances for polynomial.trailing_monic
theorem
polynomial.trailing_monic.def
{R : Type u}
[semiring R]
{p : polynomial R} :
p.trailing_monic ↔ p.trailing_coeff = 1
@[protected, instance]
noncomputable
def
polynomial.trailing_monic.decidable
{R : Type u}
[semiring R]
{p : polynomial R}
[decidable_eq R] :
Equations
- polynomial.trailing_monic.decidable = polynomial.trailing_monic.decidable._proof_1.mpr (_inst_2 p.trailing_coeff 1)
@[simp]
theorem
polynomial.trailing_monic.trailing_coeff
{R : Type u}
[semiring R]
{p : polynomial R}
(hp : p.trailing_monic) :
p.trailing_coeff = 1
@[simp]
@[simp]
@[simp]
theorem
polynomial.trailing_degree_eq_top
{R : Type u}
[semiring R]
{p : polynomial R} :
p.trailing_degree = ⊤ ↔ p = 0
theorem
polynomial.trailing_degree_eq_nat_trailing_degree
{R : Type u}
[semiring R]
{p : polynomial R}
(hp : p ≠ 0) :
theorem
polynomial.trailing_degree_eq_iff_nat_trailing_degree_eq
{R : Type u}
[semiring R]
{p : polynomial R}
{n : ℕ}
(hp : p ≠ 0) :
p.trailing_degree = ↑n ↔ p.nat_trailing_degree = n
theorem
polynomial.trailing_degree_eq_iff_nat_trailing_degree_eq_of_pos
{R : Type u}
[semiring R]
{p : polynomial R}
{n : ℕ}
(hn : 0 < n) :
p.trailing_degree = ↑n ↔ p.nat_trailing_degree = n
theorem
polynomial.nat_trailing_degree_eq_of_trailing_degree_eq_some
{R : Type u}
[semiring R]
{p : polynomial R}
{n : ℕ}
(h : p.trailing_degree = ↑n) :
p.nat_trailing_degree = n
@[simp]
theorem
polynomial.nat_trailing_degree_le_trailing_degree
{R : Type u}
[semiring R]
{p : polynomial R} :
theorem
polynomial.nat_trailing_degree_eq_of_trailing_degree_eq
{R : Type u}
{S : Type v}
[semiring R]
{p : polynomial R}
[semiring S]
{q : polynomial S}
(h : p.trailing_degree = q.trailing_degree) :
theorem
polynomial.le_trailing_degree_of_ne_zero
{R : Type u}
{n : ℕ}
[semiring R]
{p : polynomial R}
(h : p.coeff n ≠ 0) :
p.trailing_degree ≤ ↑n
theorem
polynomial.nat_trailing_degree_le_of_ne_zero
{R : Type u}
{n : ℕ}
[semiring R]
{p : polynomial R}
(h : p.coeff n ≠ 0) :
p.nat_trailing_degree ≤ n
theorem
polynomial.trailing_degree_le_trailing_degree
{R : Type u}
[semiring R]
{p q : polynomial R}
(h : q.coeff p.nat_trailing_degree ≠ 0) :
theorem
polynomial.trailing_degree_ne_of_nat_trailing_degree_ne
{R : Type u}
[semiring R]
{p : polynomial R}
{n : ℕ} :
p.nat_trailing_degree ≠ n → p.trailing_degree ≠ ↑n
theorem
polynomial.nat_trailing_degree_le_of_trailing_degree_le
{R : Type u}
[semiring R]
{p : polynomial R}
{n : ℕ}
{hp : p ≠ 0}
(H : ↑n ≤ p.trailing_degree) :
n ≤ p.nat_trailing_degree
theorem
polynomial.nat_trailing_degree_le_nat_trailing_degree
{R : Type u}
[semiring R]
{p q : polynomial R}
{hq : q ≠ 0}
(hpq : p.trailing_degree ≤ q.trailing_degree) :
@[simp]
theorem
polynomial.trailing_degree_monomial
{R : Type u}
{a : R}
{n : ℕ}
[semiring R]
(ha : a ≠ 0) :
(⇑(polynomial.monomial n) a).trailing_degree = ↑n
theorem
polynomial.nat_trailing_degree_monomial
{R : Type u}
{a : R}
{n : ℕ}
[semiring R]
(ha : a ≠ 0) :
(⇑(polynomial.monomial n) a).nat_trailing_degree = n
theorem
polynomial.nat_trailing_degree_monomial_le
{R : Type u}
{a : R}
{n : ℕ}
[semiring R] :
(⇑(polynomial.monomial n) a).nat_trailing_degree ≤ n
theorem
polynomial.le_trailing_degree_monomial
{R : Type u}
{a : R}
{n : ℕ}
[semiring R] :
↑n ≤ (⇑(polynomial.monomial n) a).trailing_degree
@[simp]
theorem
polynomial.trailing_degree_C
{R : Type u}
{a : R}
[semiring R]
(ha : a ≠ 0) :
(⇑polynomial.C a).trailing_degree = 0
theorem
polynomial.le_trailing_degree_C
{R : Type u}
{a : R}
[semiring R] :
0 ≤ (⇑polynomial.C a).trailing_degree
@[simp]
@[simp]
@[simp]
@[simp]
theorem
polynomial.trailing_degree_C_mul_X_pow
{R : Type u}
{a : R}
[semiring R]
(n : ℕ)
(ha : a ≠ 0) :
(⇑polynomial.C a * polynomial.X ^ n).trailing_degree = ↑n
theorem
polynomial.le_trailing_degree_C_mul_X_pow
{R : Type u}
[semiring R]
(n : ℕ)
(a : R) :
↑n ≤ (⇑polynomial.C a * polynomial.X ^ n).trailing_degree
theorem
polynomial.coeff_eq_zero_of_trailing_degree_lt
{R : Type u}
{n : ℕ}
[semiring R]
{p : polynomial R}
(h : ↑n < p.trailing_degree) :
theorem
polynomial.coeff_eq_zero_of_lt_nat_trailing_degree
{R : Type u}
[semiring R]
{p : polynomial R}
{n : ℕ}
(h : n < p.nat_trailing_degree) :
@[simp]
theorem
polynomial.coeff_nat_trailing_degree_pred_eq_zero
{R : Type u}
[semiring R]
{p : polynomial R}
{hp : 0 < ↑(p.nat_trailing_degree)} :
p.coeff (p.nat_trailing_degree - 1) = 0
theorem
polynomial.le_trailing_degree_X_pow
{R : Type u}
[semiring R]
(n : ℕ) :
↑n ≤ (polynomial.X ^ n).trailing_degree
@[simp]
theorem
polynomial.trailing_coeff_eq_zero
{R : Type u}
[semiring R]
{p : polynomial R} :
p.trailing_coeff = 0 ↔ p = 0
theorem
polynomial.trailing_coeff_nonzero_iff_nonzero
{R : Type u}
[semiring R]
{p : polynomial R} :
p.trailing_coeff ≠ 0 ↔ p ≠ 0
theorem
polynomial.nat_trailing_degree_mem_support_of_nonzero
{R : Type u}
[semiring R]
{p : polynomial R} :
p ≠ 0 → p.nat_trailing_degree ∈ p.support
theorem
polynomial.nat_trailing_degree_le_of_mem_supp
{R : Type u}
[semiring R]
{p : polynomial R}
(a : ℕ) :
a ∈ p.support → p.nat_trailing_degree ≤ a
theorem
polynomial.nat_trailing_degree_eq_support_min'
{R : Type u}
[semiring R]
{p : polynomial R}
(h : p ≠ 0) :
p.nat_trailing_degree = p.support.min' _
theorem
polynomial.le_nat_trailing_degree
{R : Type u}
{n : ℕ}
[semiring R]
{p : polynomial R}
(hp : p ≠ 0)
(hn : ∀ (m : ℕ), m < n → p.coeff m = 0) :
n ≤ p.nat_trailing_degree
theorem
polynomial.nat_trailing_degree_mul_X_pow
{R : Type u}
[semiring R]
{p : polynomial R}
(hp : p ≠ 0)
(n : ℕ) :
(p * polynomial.X ^ n).nat_trailing_degree = p.nat_trailing_degree + n
theorem
polynomial.le_trailing_degree_mul
{R : Type u}
[semiring R]
{p q : polynomial R} :
p.trailing_degree + q.trailing_degree ≤ (p * q).trailing_degree
theorem
polynomial.le_nat_trailing_degree_mul
{R : Type u}
[semiring R]
{p q : polynomial R}
(h : p * q ≠ 0) :
p.nat_trailing_degree + q.nat_trailing_degree ≤ (p * q).nat_trailing_degree
theorem
polynomial.coeff_mul_nat_trailing_degree_add_nat_trailing_degree
{R : Type u}
[semiring R]
{p q : polynomial R} :
(p * q).coeff (p.nat_trailing_degree + q.nat_trailing_degree) = p.trailing_coeff * q.trailing_coeff
theorem
polynomial.trailing_degree_mul'
{R : Type u}
[semiring R]
{p q : polynomial R}
(h : p.trailing_coeff * q.trailing_coeff ≠ 0) :
(p * q).trailing_degree = p.trailing_degree + q.trailing_degree
theorem
polynomial.nat_trailing_degree_mul'
{R : Type u}
[semiring R]
{p q : polynomial R}
(h : p.trailing_coeff * q.trailing_coeff ≠ 0) :
(p * q).nat_trailing_degree = p.nat_trailing_degree + q.nat_trailing_degree
theorem
polynomial.nat_trailing_degree_mul
{R : Type u}
[semiring R]
{p q : polynomial R}
[no_zero_divisors R]
(hp : p ≠ 0)
(hq : q ≠ 0) :
(p * q).nat_trailing_degree = p.nat_trailing_degree + q.nat_trailing_degree
@[simp]
theorem
polynomial.trailing_degree_one
{R : Type u}
[semiring R]
[nontrivial R] :
1.trailing_degree = 0
@[simp]
@[simp]
@[simp]
theorem
polynomial.trailing_degree_neg
{R : Type u}
[ring R]
(p : polynomial R) :
(-p).trailing_degree = p.trailing_degree
@[simp]
@[simp]
The second-lowest coefficient, or 0 for constants
Equations
- p.next_coeff_up = ite (p.nat_trailing_degree = 0) 0 (p.coeff (p.nat_trailing_degree + 1))
@[simp]
theorem
polynomial.next_coeff_up_C_eq_zero
{R : Type u}
[semiring R]
(c : R) :
(⇑polynomial.C c).next_coeff_up = 0
theorem
polynomial.next_coeff_up_of_pos_nat_trailing_degree
{R : Type u}
[semiring R]
(p : polynomial R)
(hp : 0 < p.nat_trailing_degree) :
p.next_coeff_up = p.coeff (p.nat_trailing_degree + 1)
theorem
polynomial.coeff_nat_trailing_degree_eq_zero_of_trailing_degree_lt
{R : Type u}
[semiring R]
{p q : polynomial R}
(h : p.trailing_degree < q.trailing_degree) :
q.coeff p.nat_trailing_degree = 0
theorem
polynomial.ne_zero_of_trailing_degree_lt
{R : Type u}
[semiring R]
{p : polynomial R}
{n : ℕ∞}
(h : p.trailing_degree < n) :
p ≠ 0