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.eq_C_of_nat_degree_eq_zero
{R : Type u}
[semiring R]
{p : polynomial R}
(hp : p.nat_degree = 0) :
p = ⇑polynomial.C (p.coeff 0)
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)
(hf : ⇑f p.leading_coeff ≠ 0) :
(polynomial.map f p).degree = p.degree
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) :
(polynomial.map f p).nat_degree = p.nat_degree
theorem
polynomial.leading_coeff_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) :
(polynomial.map f p).leading_coeff = ⇑f p.leading_coeff
theorem
polynomial.degree_pos_of_root
{R : Type u}
{a : R}
[semiring R]
{p : polynomial R}
(hp : p ≠ 0)
(h : p.is_root a) :
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) :
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}
(hz : polynomial.eval₂ f z p = 0)
(inj : ∀ (x : R), ⇑f x = 0 → x = 0) :
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
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) :
(polynomial.map f p).leading_coeff = ⇑f p.leading_coeff