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}
(hp : p.monic) :
p = polynomial.X ^ p.nat_degree + ∑ (i : ℕ) in finset.range p.nat_degree, (⇑polynomial.C (p.coeff i)) * polynomial.X ^ i
theorem
polynomial.ne_zero_of_monic_of_zero_ne_one
{R : Type u}
[semiring R]
{p : polynomial R}
(hp : p.monic)
(h : 0 ≠ 1) :
p ≠ 0
theorem
polynomial.ne_zero_of_ne_zero_of_monic
{R : Type u}
[semiring R]
{p q : polynomial R}
(hp : p ≠ 0)
(hq : q.monic) :
q ≠ 0
theorem
polynomial.monic_map
{R : Type u}
{S : Type v}
[semiring R]
{p : polynomial R}
[semiring S]
(f : R →+* S)
(hp : p.monic) :
(polynomial.map f p).monic
theorem
polynomial.monic_mul_C_of_leading_coeff_mul_eq_one
{R : Type u}
[semiring R]
{p : polynomial R}
[nontrivial R]
{b : R}
(hp : (p.leading_coeff) * b = 1) :
(p * ⇑polynomial.C b).monic
theorem
polynomial.monic_X_pow_add
{R : Type u}
[semiring R]
{p : polynomial R}
{n : ℕ}
(H : p.degree ≤ ↑n) :
(polynomial.X ^ (n + 1) + p).monic
theorem
polynomial.monic_mul
{R : Type u}
[semiring R]
{p q : polynomial R}
(hp : p.monic)
(hq : q.monic) :
theorem
polynomial.monic_prod_of_monic
{R : Type u}
{ι : Type y}
[comm_semiring R]
(s : finset ι)
(f : ι → polynomial R)
(hs : ∀ (i : ι), i ∈ s → (f i).monic) :
(∏ (i : ι) in s, f i).monic
theorem
polynomial.is_unit_C
{R : Type u}
[comm_semiring R]
{x : R} :
is_unit (⇑polynomial.C x) ↔ is_unit x
theorem
polynomial.eq_one_of_is_unit_of_monic
{R : Type u}
[comm_semiring R]
{p : polynomial R}
(hm : p.monic)
(hpu : is_unit p) :
p = 1
theorem
polynomial.monic.coeff_nat_degree
{R : Type u}
[comm_ring R]
{p : polynomial R}
(hp : 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}
(hp : 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}
(hp : p.monic)
(hq : 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}
(hp : p.monic)
(hq : 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)
(h : ∀ (i : ι), i ∈ s → (f i).monic) :
(∏ (i : ι) in s, f i).next_coeff = ∑ (i : ι) in s, (f i).next_coeff
theorem
polynomial.monic_X_pow_sub
{R : Type u}
[ring R]
{p : polynomial R}
{n : ℕ}
(H : p.degree ≤ ↑n) :
(polynomial.X ^ (n + 1) - p).monic
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}
(hp : (polynomial.map f p).monic) :
p.monic
@[simp]
theorem
polynomial.ne_zero_of_monic
{R : Type u}
[semiring R]
[nontrivial R]
{p : polynomial R}
(h : p.monic) :
p ≠ 0