Documentation

Mathlib.Algebra.Polynomial.Degree.Lemmas

Theory of degrees of polynomials #

Some of the main results include

theorem Polynomial.natDegree_comp_le {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} :
(p.comp q).natDegree p.natDegree * q.natDegree
theorem Polynomial.degree_pos_of_root {R : Type u} {a : R} [Semiring R] {p : Polynomial R} (hp : p 0) (h : p.IsRoot a) :
0 < p.degree
theorem Polynomial.natDegree_le_iff_coeff_eq_zero {R : Type u} {n : } [Semiring R] {p : Polynomial R} :
p.natDegree n ∀ (N : ), n < Np.coeff N = 0
theorem Polynomial.natDegree_add_le_iff_left {R : Type u} [Semiring R] {n : } (p : Polynomial R) (q : Polynomial R) (qn : q.natDegree n) :
(p + q).natDegree n p.natDegree n
theorem Polynomial.natDegree_add_le_iff_right {R : Type u} [Semiring R] {n : } (p : Polynomial R) (q : Polynomial R) (pn : p.natDegree n) :
(p + q).natDegree n q.natDegree n
theorem Polynomial.natDegree_C_mul_le {R : Type u} [Semiring R] (a : R) (f : Polynomial R) :
(Polynomial.C a * f).natDegree f.natDegree
theorem Polynomial.natDegree_mul_C_le {R : Type u} [Semiring R] (f : Polynomial R) (a : R) :
(f * Polynomial.C a).natDegree f.natDegree
theorem Polynomial.eq_natDegree_of_le_mem_support {R : Type u} {n : } [Semiring R] {p : Polynomial R} (pn : p.natDegree n) (ns : n p.support) :
p.natDegree = n
theorem Polynomial.natDegree_C_mul_eq_of_mul_eq_one {R : Type u} {a : R} [Semiring R] {p : Polynomial R} {ai : R} (au : ai * a = 1) :
(Polynomial.C a * p).natDegree = p.natDegree
theorem Polynomial.natDegree_mul_C_eq_of_mul_eq_one {R : Type u} {a : R} [Semiring R] {p : Polynomial R} {ai : R} (au : a * ai = 1) :
(p * Polynomial.C a).natDegree = p.natDegree
theorem Polynomial.natDegree_mul_C_eq_of_mul_ne_zero {R : Type u} {a : R} [Semiring R] {p : Polynomial R} (h : p.leadingCoeff * a 0) :
(p * Polynomial.C a).natDegree = p.natDegree

Although not explicitly stated, the assumptions of lemma nat_degree_mul_C_eq_of_mul_ne_zero force the polynomial p to be non-zero, via p.leading_coeff ≠ 0.

theorem Polynomial.natDegree_C_mul_eq_of_mul_ne_zero {R : Type u} {a : R} [Semiring R] {p : Polynomial R} (h : a * p.leadingCoeff 0) :
(Polynomial.C a * p).natDegree = p.natDegree

Although not explicitly stated, the assumptions of lemma nat_degree_C_mul_eq_of_mul_ne_zero force the polynomial p to be non-zero, via p.leading_coeff ≠ 0.

theorem Polynomial.natDegree_add_coeff_mul {R : Type u} [Semiring R] (f : Polynomial R) (g : Polynomial R) :
(f * g).coeff (f.natDegree + g.natDegree) = f.coeff f.natDegree * g.coeff g.natDegree
theorem Polynomial.natDegree_lt_coeff_mul {R : Type u} {m : } {n : } [Semiring R] {p : Polynomial R} {q : Polynomial R} (h : p.natDegree + q.natDegree < m + n) :
(p * q).coeff (m + n) = 0
theorem Polynomial.coeff_mul_of_natDegree_le {R : Type u} {m : } {n : } [Semiring R] {p : Polynomial R} {q : Polynomial R} (pm : p.natDegree m) (qn : q.natDegree n) :
(p * q).coeff (m + n) = p.coeff m * q.coeff n
theorem Polynomial.coeff_pow_of_natDegree_le {R : Type u} {m : } {n : } [Semiring R] {p : Polynomial R} (pn : p.natDegree n) :
(p ^ m).coeff (m * n) = p.coeff n ^ m
theorem Polynomial.coeff_pow_eq_ite_of_natDegree_le_of_le {R : Type u} {m : } {n : } [Semiring R] {p : Polynomial R} {o : } (pn : p.natDegree n) (mno : m * n o) :
(p ^ m).coeff o = if o = m * n then p.coeff n ^ m else 0
theorem Polynomial.coeff_add_eq_left_of_lt {R : Type u} {n : } [Semiring R] {p : Polynomial R} {q : Polynomial R} (qn : q.natDegree < n) :
(p + q).coeff n = p.coeff n
theorem Polynomial.coeff_add_eq_right_of_lt {R : Type u} {n : } [Semiring R] {p : Polynomial R} {q : Polynomial R} (pn : p.natDegree < n) :
(p + q).coeff n = q.coeff n
theorem Polynomial.degree_sum_eq_of_disjoint {R : Type u} {S : Type v} [Semiring R] (f : SPolynomial R) (s : Finset S) (h : {i : S | i s f i 0}.Pairwise (Ne on Polynomial.degree f)) :
(s.sum f).degree = s.sup fun (i : S) => (f i).degree
theorem Polynomial.natDegree_sum_eq_of_disjoint {R : Type u} {S : Type v} [Semiring R] (f : SPolynomial R) (s : Finset S) (h : {i : S | i s f i 0}.Pairwise (Ne on Polynomial.natDegree f)) :
(s.sum f).natDegree = s.sup fun (i : S) => (f i).natDegree
theorem Polynomial.natDegree_pos_of_eval₂_root {R : Type u} {S : Type v} [Semiring R] [Semiring S] {p : Polynomial R} (hp : p 0) (f : R →+* S) {z : S} (hz : Polynomial.eval₂ f z p = 0) (inj : ∀ (x : R), f x = 0x = 0) :
0 < p.natDegree
theorem Polynomial.degree_pos_of_eval₂_root {R : Type u} {S : Type v} [Semiring R] [Semiring S] {p : Polynomial R} (hp : p 0) (f : R →+* S) {z : S} (hz : Polynomial.eval₂ f z p = 0) (inj : ∀ (x : R), f x = 0x = 0) :
0 < p.degree
@[simp]
theorem Polynomial.coe_lt_degree {R : Type u} [Semiring R] {p : Polynomial R} {n : } :
n < p.degree n < p.natDegree
@[simp]
theorem Polynomial.degree_map_eq_iff {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} :
(Polynomial.map f p).degree = p.degree f p.leadingCoeff 0 p = 0
@[simp]
theorem Polynomial.natDegree_map_eq_iff {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} :
(Polynomial.map f p).natDegree = p.natDegree f p.leadingCoeff 0 p.natDegree = 0
theorem Polynomial.natDegree_pos_of_nextCoeff_ne_zero {R : Type u} [Semiring R] {p : Polynomial R} (h : p.nextCoeff 0) :
0 < p.natDegree
theorem Polynomial.natDegree_sub {R : Type u} [Ring R] {p : Polynomial R} {q : Polynomial R} :
(p - q).natDegree = (q - p).natDegree
theorem Polynomial.natDegree_sub_le_iff_left {R : Type u} {n : } [Ring R] {p : Polynomial R} {q : Polynomial R} (qn : q.natDegree n) :
(p - q).natDegree n p.natDegree n
theorem Polynomial.natDegree_sub_le_iff_right {R : Type u} {n : } [Ring R] {p : Polynomial R} {q : Polynomial R} (pn : p.natDegree n) :
(p - q).natDegree n q.natDegree n
theorem Polynomial.coeff_sub_eq_left_of_lt {R : Type u} {n : } [Ring R] {p : Polynomial R} {q : Polynomial R} (dg : q.natDegree < n) :
(p - q).coeff n = p.coeff n
theorem Polynomial.coeff_sub_eq_neg_right_of_lt {R : Type u} {n : } [Ring R] {p : Polynomial R} {q : Polynomial R} (df : p.natDegree < n) :
(p - q).coeff n = -q.coeff n
theorem Polynomial.degree_mul_C {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} {a : R} (a0 : a 0) :
(p * Polynomial.C a).degree = p.degree
theorem Polynomial.degree_C_mul {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} {a : R} (a0 : a 0) :
(Polynomial.C a * p).degree = p.degree
theorem Polynomial.natDegree_mul_C {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} {a : R} (a0 : a 0) :
(p * Polynomial.C a).natDegree = p.natDegree
theorem Polynomial.natDegree_C_mul {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} {a : R} (a0 : a 0) :
(Polynomial.C a * p).natDegree = p.natDegree
@[simp]
theorem Polynomial.nextCoeff_C_mul_X_add_C {R : Type u} [Semiring R] {a : R} (ha : a 0) (c : R) :
(Polynomial.C a * Polynomial.X + Polynomial.C c).nextCoeff = c
theorem Polynomial.natDegree_eq_one {R : Type u} [Semiring R] {p : Polynomial R} :
p.natDegree = 1 ∃ (a : R), a 0 ∃ (b : R), Polynomial.C a * Polynomial.X + Polynomial.C b = p
theorem Polynomial.natDegree_comp {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} {q : Polynomial R} :
(p.comp q).natDegree = p.natDegree * q.natDegree
@[simp]
theorem Polynomial.natDegree_iterate_comp {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} {q : Polynomial R} (k : ) :
(p.comp^[k] q).natDegree = p.natDegree ^ k * q.natDegree
theorem Polynomial.leadingCoeff_comp {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} {q : Polynomial R} (hq : q.natDegree 0) :
(p.comp q).leadingCoeff = p.leadingCoeff * q.leadingCoeff ^ p.natDegree

Useful lemmas for the "monicization" of a nonzero polynomial p.

@[simp]
theorem Polynomial.irreducible_mul_leadingCoeff_inv {K : Type u_1} [DivisionRing K] {p : Polynomial K} :
Irreducible (p * Polynomial.C p.leadingCoeff⁻¹) Irreducible p
@[simp]
theorem Polynomial.dvd_mul_leadingCoeff_inv {K : Type u_1} [DivisionRing K] {p : Polynomial K} {q : Polynomial K} (hp0 : p 0) :
q p * Polynomial.C p.leadingCoeff⁻¹ q p
theorem Polynomial.monic_mul_leadingCoeff_inv {K : Type u_1} [DivisionRing K] {p : Polynomial K} (h : p 0) :
(p * Polynomial.C p.leadingCoeff⁻¹).Monic
@[simp]
theorem Polynomial.degree_leadingCoeff_inv {K : Type u_1} [DivisionRing K] {p : Polynomial K} (hp0 : p 0) :
(Polynomial.C p.leadingCoeff⁻¹).degree = 0
theorem Polynomial.degree_mul_leadingCoeff_inv {K : Type u_1} [DivisionRing K] (p : Polynomial K) {q : Polynomial K} (h : q 0) :
(p * Polynomial.C q.leadingCoeff⁻¹).degree = p.degree
theorem Polynomial.natDegree_mul_leadingCoeff_inv {K : Type u_1} [DivisionRing K] (p : Polynomial K) {q : Polynomial K} (h : q 0) :
(p * Polynomial.C q.leadingCoeff⁻¹).natDegree = p.natDegree
theorem Polynomial.degree_mul_leadingCoeff_self_inv {K : Type u_1} [DivisionRing K] (p : Polynomial K) :
(p * Polynomial.C p.leadingCoeff⁻¹).degree = p.degree
theorem Polynomial.natDegree_mul_leadingCoeff_self_inv {K : Type u_1} [DivisionRing K] (p : Polynomial K) :
(p * Polynomial.C p.leadingCoeff⁻¹).natDegree = p.natDegree
@[simp]
theorem Polynomial.degree_add_degree_leadingCoeff_inv {K : Type u_1} [DivisionRing K] (p : Polynomial K) :
p.degree + (Polynomial.C p.leadingCoeff⁻¹).degree = p.degree