Theory of degrees of polynomials
Some of the main results include
nat_degree_comp_le: The degree of the composition is at most the product of degrees
theorem
polynomial.nat_degree_comp_le
{R : Type u}
[semiring R]
{p q : polynomial R} :
(p.comp q).nat_degree ≤ p.nat_degree * q.nat_degree
theorem
polynomial.degree_map_le
{R : Type u}
{S : Type v}
[semiring R]
{p : polynomial R}
[semiring S]
(f : R →+* S) :
(polynomial.map f p).degree ≤ p.degree
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) :
⇑f p.leading_coeff ≠ 0 → (polynomial.map f p).degree = 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 = 0 → x = 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} :
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) :
(polynomial.map f p).degree = p.degree
theorem
polynomial.degree_map'
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
{f : R →+* S}
(hf : function.injective ⇑f)
(p : polynomial R) :
(polynomial.map f p).degree = p.degree
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) :
(polynomial.map f p).nat_degree = p.nat_degree