mathlib documentation

data.polynomial.degree

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_le {R : Type u} {S : Type v} [semiring R] {p : polynomial R} [semiring S] (f : R →+* S) :

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) :

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) :

theorem polynomial.degree_pos_of_root {R : Type u} {a : R} [semiring R] {p : polynomial R} :
p 0p.is_root a0 < p.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} :
polynomial.eval₂ f z p = 0(∀ (x : R), f x = 0x = 0)0 < p.nat_degree

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} :
polynomial.eval₂ f z p = 0(∀ (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) :