mathlib3 documentation

data.polynomial.degree.lemmas

Theory of degrees of polynomials #

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

Some of the main results include

theorem polynomial.degree_pos_of_root {R : Type u} {a : R} [semiring R] {p : polynomial R} (hp : p 0) (h : p.is_root a) :
0 < p.degree
theorem polynomial.nat_degree_le_iff_coeff_eq_zero {R : Type u} {n : } [semiring R] {p : polynomial R} :
p.nat_degree n (N : ), n < N p.coeff N = 0
theorem polynomial.nat_degree_add_le_iff_left {R : Type u} [semiring R] {n : } (p q : polynomial R) (qn : q.nat_degree n) :
theorem polynomial.nat_degree_add_le_iff_right {R : Type u} [semiring R] {n : } (p q : polynomial R) (pn : p.nat_degree n) :
theorem polynomial.eq_nat_degree_of_le_mem_support {R : Type u} {n : } [semiring R] {p : polynomial R} (pn : p.nat_degree n) (ns : n p.support) :
theorem polynomial.nat_degree_C_mul_eq_of_mul_eq_one {R : Type u} {a : R} [semiring R] {p : polynomial R} {ai : R} (au : ai * a = 1) :
theorem polynomial.nat_degree_mul_C_eq_of_mul_eq_one {R : Type u} {a : R} [semiring R] {p : polynomial R} {ai : R} (au : a * ai = 1) :

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.

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.nat_degree_lt_coeff_mul {R : Type u} {m n : } [semiring R] {p q : polynomial R} (h : p.nat_degree + q.nat_degree < m + n) :
(p * q).coeff (m + n) = 0
theorem polynomial.coeff_mul_of_nat_degree_le {R : Type u} {m n : } [semiring R] {p q : polynomial R} (pm : p.nat_degree m) (qn : q.nat_degree n) :
(p * q).coeff (m + n) = p.coeff m * q.coeff n
theorem polynomial.coeff_pow_of_nat_degree_le {R : Type u} {m n : } [semiring R] {p : polynomial R} (pn : p.nat_degree n) :
(p ^ m).coeff (n * m) = p.coeff n ^ m
theorem polynomial.coeff_add_eq_left_of_lt {R : Type u} {n : } [semiring R] {p q : polynomial R} (qn : q.nat_degree < n) :
(p + q).coeff n = p.coeff n
theorem polynomial.coeff_add_eq_right_of_lt {R : Type u} {n : } [semiring R] {p q : polynomial R} (pn : p.nat_degree < n) :
(p + q).coeff n = q.coeff n
theorem polynomial.degree_sum_eq_of_disjoint {R : Type u} {S : Type v} [semiring R] (f : S polynomial R) (s : finset S) (h : {i : S | i s f i 0}.pairwise (ne on polynomial.degree f)) :
(s.sum f).degree = s.sup (λ (i : S), (f i).degree)
theorem polynomial.nat_degree_sum_eq_of_disjoint {R : Type u} {S : Type v} [semiring R] (f : S polynomial R) (s : finset S) (h : {i : S | i s f i 0}.pairwise (ne on polynomial.nat_degree f)) :
(s.sum f).nat_degree = s.sup (λ (i : S), (f i).nat_degree)
theorem polynomial.nat_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 = 0 x = 0) :
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 = 0 x = 0) :
0 < p.degree
@[simp]
theorem polynomial.coe_lt_degree {R : Type u} [semiring R] {p : polynomial R} {n : } :
theorem polynomial.nat_degree_sub {R : Type u} [ring R] {p q : polynomial R} :
(p - q).nat_degree = (q - p).nat_degree
theorem polynomial.nat_degree_sub_le_iff_left {R : Type u} {n : } [ring R] {p q : polynomial R} (qn : q.nat_degree n) :
theorem polynomial.nat_degree_sub_le_iff_right {R : Type u} {n : } [ring R] {p q : polynomial R} (pn : p.nat_degree n) :
theorem polynomial.coeff_sub_eq_left_of_lt {R : Type u} {n : } [ring R] {p q : polynomial R} (dg : q.nat_degree < n) :
(p - q).coeff n = p.coeff n
theorem polynomial.coeff_sub_eq_neg_right_of_lt {R : Type u} {n : } [ring R] {p q : polynomial R} (df : p.nat_degree < n) :
(p - q).coeff n = -q.coeff n
theorem polynomial.degree_mul_C {R : Type u} {a : R} [semiring R] [no_zero_divisors R] {p : polynomial R} (a0 : a 0) :
theorem polynomial.degree_C_mul {R : Type u} {a : R} [semiring R] [no_zero_divisors R] {p : polynomial R} (a0 : a 0) :
theorem polynomial.nat_degree_mul_C {R : Type u} {a : R} [semiring R] [no_zero_divisors R] {p : polynomial R} (a0 : a 0) :
theorem polynomial.nat_degree_C_mul {R : Type u} {a : R} [semiring R] [no_zero_divisors R] {p : polynomial R} (a0 : a 0) :