Theory of monic polynomials
We give several tools for proving that polynomials are monic, e.g.
monic_mul, monic_map.
theorem
polynomial.monic.as_sum
{R : Type u}
[semiring R]
{p : polynomial R} :
p.monic → p = polynomial.X ^ p.nat_degree + (finset.range p.nat_degree).sum (λ (i : ℕ), ⇑polynomial.C (p.coeff i) * polynomial.X ^ i)
theorem
polynomial.monic_map
{R : Type u}
{S : Type v}
[semiring R]
{p : polynomial R}
[semiring S]
(f : R →+* S) :
p.monic → (polynomial.map f p).monic
theorem
polynomial.monic_prod_of_monic
{R : Type u}
{ι : Type y}
[comm_semiring R]
(s : finset ι)
(f : ι → polynomial R) :
theorem
polynomial.is_unit_C
{R : Type u}
[comm_semiring R]
{x : R} :
is_unit (⇑polynomial.C x) ↔ is_unit x
theorem
polynomial.monic.coeff_nat_degree
{R : Type u}
[comm_ring R]
{p : polynomial R} :
p.monic → p.coeff p.nat_degree = 1
@[simp]
theorem
polynomial.monic.degree_eq_zero_iff_eq_one
{R : Type u}
[comm_ring R]
{p : polynomial R} :
p.monic → (p.nat_degree = 0 ↔ p = 1)
theorem
polynomial.monic.nat_degree_mul
{R : Type u}
[comm_ring R]
[nontrivial R]
{p q : polynomial R} :
p.monic → q.monic → (p * q).nat_degree = p.nat_degree + q.nat_degree
theorem
polynomial.monic.next_coeff_mul
{R : Type u}
[comm_ring R]
{p q : polynomial R} :
p.monic → q.monic → (p * q).next_coeff = p.next_coeff + q.next_coeff
theorem
polynomial.monic.next_coeff_prod
{R : Type u}
{ι : Type y}
[comm_ring R]
(s : finset ι)
(f : ι → polynomial R) :
(∀ (i : ι), i ∈ s → (f i).monic) → (s.prod (λ (i : ι), f i)).next_coeff = s.sum (λ (i : ι), (f i).next_coeff)
theorem
polynomial.leading_coeff_of_injective
{R : Type u}
{S : Type v}
[ring R]
[semiring S]
{f : R →+* S}
(hf : function.injective ⇑f)
(p : polynomial R) :
(polynomial.map f p).leading_coeff = ⇑f p.leading_coeff
theorem
polynomial.monic_of_injective
{R : Type u}
{S : Type v}
[ring R]
[semiring S]
{f : R →+* S}
(hf : function.injective ⇑f)
{p : polynomial R} :
(polynomial.map f p).monic → p.monic
@[simp]