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
- p.trailing_degree = p.support.inf some
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 = 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)
theorem
polynomial.trailing_monic.def
{R : Type u}
[semiring R]
{p : polynomial R} :
p.trailing_monic ↔ p.trailing_coeff = 1
@[instance]
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]
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 : ℕ}
(a : 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_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_monomial
{R : Type u}
{a : R}
[semiring R]
(n : ℕ)
(ha : a ≠ 0) :
((⇑polynomial.C a) * polynomial.X ^ n).trailing_degree = ↑n
theorem
polynomial.monomial_le_trailing_degree
{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_C_mul_X_pow
{R : Type u}
[semiring R]
(r : R)
(n : ℕ) :
↑n ≤ ((⇑polynomial.C r) * polynomial.X ^ n).trailing_degree
theorem
polynomial.le_trailing_degree_X_pow
{R : Type u}
[semiring R]
(n : ℕ) :
↑n ≤ (polynomial.X ^ n).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 : with_top ℕ}
(h : p.trailing_degree < n) :
p ≠ 0