mathlib documentation

data.polynomial.degree.lemmas

Theory of degrees of polynomials #

Some of the main results include

theorem polynomial.nat_degree_comp_le {R : Type u} [semiring R] {p q : polynomial R} :
theorem polynomial.degree_map_eq_of_leading_coeff_ne_zero {R : Type u} {S : Type v} [semiring R] {p : polynomial R} [semiring S] (f : R →+* S) (hf : f p.leading_coeff 0) :
theorem polynomial.nat_degree_map_of_leading_coeff_ne_zero {R : Type u} {S : Type v} [semiring R] {p : polynomial R} [semiring S] (f : R →+* S) (hf : f p.leading_coeff 0) :
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 < Np.coeff N = 0
theorem polynomial.nat_degree_C_mul_le {R : Type u} [semiring R] (a : R) (f : polynomial R) :
theorem polynomial.nat_degree_mul_C_le {R : Type u} [semiring R] (f : polynomial R) (a : R) :
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) :
theorem polynomial.nat_degree_mul_C_eq_of_mul_ne_zero {R : Type u} {a : R} [semiring R] {p : polynomial R} (h : (p.leading_coeff) * a 0) :

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. Lemma nat_degree_mul_C_eq_of_no_zero_divisors below separates cases, in order to overcome this hurdle.

theorem polynomial.nat_degree_C_mul_eq_of_mul_ne_zero {R : Type u} {a : R} [semiring R] {p : polynomial R} (h : a * 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. Lemma nat_degree_C_mul_eq_of_no_zero_divisors below separates cases, in order to overcome this hurdle.

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.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 = 0x = 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 = 0x = 0) :
0 < p.degree
theorem polynomial.degree_map_eq_of_injective {R : Type u} {S : Type v} [semiring R] [semiring S] {f : R →+* S} (hf : function.injective f) (p : polynomial R) :
theorem polynomial.degree_map' {R : Type u} {S : Type v} [semiring R] [semiring S] {f : R →+* S} (hf : function.injective f) (p : polynomial R) :
theorem polynomial.nat_degree_map' {R : Type u} {S : Type v} [semiring R] [semiring S] {f : R →+* S} (hf : function.injective f) (p : polynomial R) :
theorem polynomial.leading_coeff_map' {R : Type u} {S : Type v} [semiring R] [semiring S] {f : R →+* S} (hf : function.injective f) (p : polynomial R) :
theorem polynomial.next_coeff_map {R : Type u} {S : Type v} [semiring R] [semiring S] {f : R →+* S} (hf : function.injective f) (p : polynomial R) :