mathlib3 documentation

data.polynomial.degree.trailing_degree

Trailing degree of univariate polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main definitions #

Converts most results about degree, nat_degree and leading_coeff to results about the bottom end of a polynomial

source
def polynomial.trailing_degree {R : Type u} [semiring R] (p : polynomial R) :
ℕ∞

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
source
theorem polynomial.trailing_degree_lt_wf {R : Type u} [semiring R] :
well_founded (λ (p q : polynomial R), p.trailing_degree < q.trailing_degree)
source
def polynomial.nat_trailing_degree {R : Type u} [semiring R] (p : polynomial R) :
ℕ

nat_trailing_degree p forces trailing_degree p to ℕ, by defining nat_trailing_degree ⊤ = 0.

Equations
source
def polynomial.trailing_coeff {R : Type u} [semiring R] (p : polynomial R) :
R

trailing_coeff p gives the coefficient of the smallest power of X in p

Equations
source
def polynomial.trailing_monic {R : Type u} [semiring R] (p : polynomial R) :
Prop

a polynomial is monic_at if its trailing coefficient is 1

Equations
Instances for polynomial.trailing_monic
source
theorem polynomial.trailing_monic.def {R : Type u} [semiring R] {p : polynomial R} :
p.trailing_monic ↔ p.trailing_coeff = 1
source
@[protected, instance]
def polynomial.trailing_monic.decidable {R : Type u} [semiring R] {p : polynomial R} [decidable_eq R] :
decidable p.trailing_monic
Equations
source
@[simp]
theorem polynomial.trailing_monic.trailing_coeff {R : Type u} [semiring R] {p : polynomial R} (hp : p.trailing_monic) :
p.trailing_coeff = 1
source
@[simp]
theorem polynomial.trailing_degree_zero {R : Type u} [semiring R] :
0.trailing_degree = ⊤
source
@[simp]
theorem polynomial.trailing_coeff_zero {R : Type u} [semiring R] :
0.trailing_coeff = 0
source
@[simp]
theorem polynomial.nat_trailing_degree_zero {R : Type u} [semiring R] :
0.nat_trailing_degree = 0
source
theorem polynomial.trailing_degree_eq_top {R : Type u} [semiring R] {p : polynomial R} :
p.trailing_degree = ⊤ ↔ p = 0
source
theorem polynomial.trailing_degree_eq_nat_trailing_degree {R : Type u} [semiring R] {p : polynomial R} (hp : p ≠ 0) :
p.trailing_degree = ↑(p.nat_trailing_degree)
source
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
source
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
source
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
source
@[simp]
theorem polynomial.nat_trailing_degree_le_trailing_degree {R : Type u} [semiring R] {p : polynomial R} :
↑(p.nat_trailing_degree) ≤ p.trailing_degree
source
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) :
p.nat_trailing_degree = q.nat_trailing_degree
source
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
source
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
source
theorem polynomial.trailing_degree_le_trailing_degree {R : Type u} [semiring R] {p q : polynomial R} (h : q.coeff p.nat_trailing_degree ≠ 0) :
q.trailing_degree ≤ p.trailing_degree
source
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
source
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
source
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) :
p.nat_trailing_degree ≤ q.nat_trailing_degree
source
@[simp]
theorem polynomial.trailing_degree_monomial {R : Type u} {a : R} {n : ℕ} [semiring R] (ha : a ≠ 0) :
(⇑(polynomial.monomial n) a).trailing_degree = ↑n
source
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
source
theorem polynomial.nat_trailing_degree_monomial_le {R : Type u} {a : R} {n : ℕ} [semiring R] :
(⇑(polynomial.monomial n) a).nat_trailing_degree ≤ n
source
theorem polynomial.le_trailing_degree_monomial {R : Type u} {a : R} {n : ℕ} [semiring R] :
↑n ≤ (⇑(polynomial.monomial n) a).trailing_degree
source
@[simp]
theorem polynomial.trailing_degree_C {R : Type u} {a : R} [semiring R] (ha : a ≠ 0) :
(⇑polynomial.C a).trailing_degree = 0
source
theorem polynomial.le_trailing_degree_C {R : Type u} {a : R} [semiring R] :
0 ≤ (⇑polynomial.C a).trailing_degree
source
theorem polynomial.trailing_degree_one_le {R : Type u} [semiring R] :
0 ≤ 1.trailing_degree
source
@[simp]
theorem polynomial.nat_trailing_degree_C {R : Type u} [semiring R] (a : R) :
(⇑polynomial.C a).nat_trailing_degree = 0
source
@[simp]
theorem polynomial.nat_trailing_degree_one {R : Type u} [semiring R] :
1.nat_trailing_degree = 0
source
@[simp]
theorem polynomial.nat_trailing_degree_nat_cast {R : Type u} [semiring R] (n : ℕ) :
↑n.nat_trailing_degree = 0
source
@[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
source
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
source
theorem polynomial.coeff_eq_zero_of_trailing_degree_lt {R : Type u} {n : ℕ} [semiring R] {p : polynomial R} (h : ↑n < p.trailing_degree) :
p.coeff n = 0
source
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) :
p.coeff n = 0
source
@[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
source
theorem polynomial.le_trailing_degree_X_pow {R : Type u} [semiring R] (n : ℕ) :
↑n ≤ (polynomial.X ^ n).trailing_degree
source
theorem polynomial.le_trailing_degree_X {R : Type u} [semiring R] :
1 ≤ polynomial.X.trailing_degree
source
theorem polynomial.nat_trailing_degree_X_le {R : Type u} [semiring R] :
polynomial.X.nat_trailing_degree ≤ 1
source
@[simp]
theorem polynomial.trailing_coeff_eq_zero {R : Type u} [semiring R] {p : polynomial R} :
p.trailing_coeff = 0 ↔ p = 0
source
theorem polynomial.trailing_coeff_nonzero_iff_nonzero {R : Type u} [semiring R] {p : polynomial R} :
p.trailing_coeff ≠ 0 ↔ p ≠ 0
source
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
source
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
source
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' _
source
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
source
theorem polynomial.nat_trailing_degree_le_nat_degree {R : Type u} [semiring R] (p : polynomial R) :
p.nat_trailing_degree ≤ p.nat_degree
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
@[simp]
theorem polynomial.trailing_degree_one {R : Type u} [semiring R] [nontrivial R] :
1.trailing_degree = 0
source
@[simp]
theorem polynomial.trailing_degree_X {R : Type u} [semiring R] [nontrivial R] :
polynomial.X.trailing_degree = 1
source
@[simp]
theorem polynomial.nat_trailing_degree_X {R : Type u} [semiring R] [nontrivial R] :
polynomial.X.nat_trailing_degree = 1
source
@[simp]
theorem polynomial.trailing_degree_neg {R : Type u} [ring R] (p : polynomial R) :
(-p).trailing_degree = p.trailing_degree
source
@[simp]
theorem polynomial.nat_trailing_degree_neg {R : Type u} [ring R] (p : polynomial R) :
(-p).nat_trailing_degree = p.nat_trailing_degree
source
@[simp]
theorem polynomial.nat_trailing_degree_int_cast {R : Type u} [ring R] (n : ℤ) :
↑n.nat_trailing_degree = 0
source
def polynomial.next_coeff_up {R : Type u} [semiring R] (p : polynomial R) :
R

The second-lowest coefficient, or 0 for constants

Equations
source
@[simp]
theorem polynomial.next_coeff_up_C_eq_zero {R : Type u} [semiring R] (c : R) :
(⇑polynomial.C c).next_coeff_up = 0
source
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)
source
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
source
theorem polynomial.ne_zero_of_trailing_degree_lt {R : Type u} [semiring R] {p : polynomial R} {n : ℕ∞} (h : p.trailing_degree < n) :
p ≠ 0