Theory of monic polynomials #
We give several tools for proving that polynomials are monic, e.g.
monic.mul
, monic.map
, monic.pow
.
theorem
polynomial.monic.as_sum
{R : Type u}
[semiring R]
{p : R[X]}
(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.monic.map
{R : Type u}
{S : Type v}
[semiring R]
{p : R[X]}
[semiring S]
(f : R →+* S)
(hp : p.monic) :
(polynomial.map f p).monic
theorem
polynomial.monic_C_mul_of_mul_leading_coeff_eq_one
{R : Type u}
[semiring R]
{p : R[X]}
{b : R}
(hp : b * p.leading_coeff = 1) :
((⇑polynomial.C b) * p).monic
theorem
polynomial.monic_mul_C_of_leading_coeff_mul_eq_one
{R : Type u}
[semiring R]
{p : R[X]}
{b : R}
(hp : (p.leading_coeff) * b = 1) :
(p * ⇑polynomial.C b).monic
@[simp]
theorem
polynomial.monic.nat_degree_eq_zero_iff_eq_one
{R : Type u}
[semiring R]
{p : R[X]}
(hp : p.monic) :
p.nat_degree = 0 ↔ p = 1
theorem
polynomial.monic.nat_degree_mul
{R : Type u}
[semiring R]
{p q : R[X]}
(hp : p.monic)
(hq : q.monic) :
(p * q).nat_degree = p.nat_degree + q.nat_degree
theorem
polynomial.monic.nat_degree_mul'
{R : Type u}
[semiring R]
{p q : R[X]}
(hp : p.monic)
(hq : q ≠ 0) :
(p * q).nat_degree = p.nat_degree + q.nat_degree
theorem
polynomial.monic.nat_degree_mul_comm
{R : Type u}
[semiring R]
{p : R[X]}
(hp : p.monic)
(q : R[X]) :
(p * q).nat_degree = (q * p).nat_degree
theorem
polynomial.monic.next_coeff_mul
{R : Type u}
[semiring R]
{p q : R[X]}
(hp : p.monic)
(hq : q.monic) :
(p * q).next_coeff = p.next_coeff + q.next_coeff
theorem
polynomial.monic.eq_one_of_map_eq_one
{R : Type u}
[semiring R]
{p : R[X]}
{S : Type u_1}
[semiring S]
[nontrivial S]
(f : R →+* S)
(hp : p.monic)
(map_eq : polynomial.map f p = 1) :
p = 1
theorem
polynomial.monic.nat_degree_pow
{R : Type u}
[semiring R]
{p : R[X]}
(hp : p.monic)
(n : ℕ) :
(p ^ n).nat_degree = n * p.nat_degree
@[simp]
theorem
polynomial.nat_degree_pow_X_add_C
{R : Type u}
[semiring R]
[nontrivial R]
(n : ℕ)
(r : R) :
((polynomial.X + ⇑polynomial.C r) ^ n).nat_degree = n
theorem
polynomial.monic_multiset_prod_of_monic
{R : Type u}
{ι : Type y}
[comm_semiring R]
(t : multiset ι)
(f : ι → R[X])
(ht : ∀ (i : ι), i ∈ t → (f i).monic) :
(multiset.map f t).prod.monic
theorem
polynomial.monic_prod_of_monic
{R : Type u}
{ι : Type y}
[comm_semiring R]
(s : finset ι)
(f : ι → R[X])
(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 : R[X]}
(hm : p.monic)
(hpu : is_unit p) :
p = 1
theorem
polynomial.monic.next_coeff_multiset_prod
{R : Type u}
{ι : Type y}
[comm_semiring R]
(t : multiset ι)
(f : ι → R[X])
(h : ∀ (i : ι), i ∈ t → (f i).monic) :
(multiset.map f t).prod.next_coeff = (multiset.map (λ (i : ι), (f i).next_coeff) t).sum
theorem
polynomial.monic.next_coeff_prod
{R : Type u}
{ι : Type y}
[comm_semiring R]
(s : finset ι)
(f : ι → R[X])
(h : ∀ (i : ι), i ∈ s → (f i).monic) :
(∏ (i : ι) in s, f i).next_coeff = ∑ (i : ι) in s, (f i).next_coeff
@[simp]
theorem
polynomial.monic.nat_degree_map
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
[nontrivial S]
{P : R[X]}
(hmo : P.monic)
(f : R →+* S) :
(polynomial.map f P).nat_degree = P.nat_degree
@[simp]
theorem
polynomial.monic.degree_map
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
[nontrivial S]
{P : R[X]}
(hmo : P.monic)
(f : R →+* S) :
(polynomial.map f P).degree = 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 : R[X]) :
(polynomial.map f p).degree = p.degree
theorem
polynomial.nat_degree_map_eq_of_injective
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
{f : R →+* S}
(hf : function.injective ⇑f)
(p : R[X]) :
(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 : R[X]) :
(polynomial.map f p).leading_coeff = ⇑f p.leading_coeff
theorem
polynomial.next_coeff_map
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
{f : R →+* S}
(hf : function.injective ⇑f)
(p : R[X]) :
(polynomial.map f p).next_coeff = ⇑f p.next_coeff
theorem
polynomial.leading_coeff_of_injective
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
{f : R →+* S}
(hf : function.injective ⇑f)
(p : R[X]) :
(polynomial.map f p).leading_coeff = ⇑f p.leading_coeff
theorem
polynomial.monic_of_injective
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
{f : R →+* S}
(hf : function.injective ⇑f)
{p : R[X]}
(hp : (polynomial.map f p).monic) :
p.monic
theorem
polynomial.monic_X_pow_sub_C
{R : Type u}
[ring R]
(a : R)
{n : ℕ}
(h : n ≠ 0) :
(polynomial.X ^ n - ⇑polynomial.C a).monic
X ^ n - a
is monic.
theorem
polynomial.not_is_unit_X_pow_sub_one
(R : Type u_1)
[comm_ring R]
[nontrivial R]
(n : ℕ) :
¬is_unit (polynomial.X ^ n - 1)
@[simp]
theorem
polynomial.monic.mul_nat_degree_lt_iff
{R : Type u}
[semiring R]
{p : R[X]}
(h : p.monic)
{q : R[X]} :
(p * q).nat_degree < p.nat_degree ↔ p ≠ 1 ∧ q = 0
theorem
polynomial.degree_smul_of_smul_regular
{R : Type u}
[semiring R]
{S : Type u_1}
[monoid S]
[distrib_mul_action S R]
{k : S}
(p : R[X])
(h : is_smul_regular R k) :
theorem
polynomial.nat_degree_smul_of_smul_regular
{R : Type u}
[semiring R]
{S : Type u_1}
[monoid S]
[distrib_mul_action S R]
{k : S}
(p : R[X])
(h : is_smul_regular R k) :
(k • p).nat_degree = p.nat_degree
theorem
polynomial.leading_coeff_smul_of_smul_regular
{R : Type u}
[semiring R]
{S : Type u_1}
[monoid S]
[distrib_mul_action S R]
{k : S}
(p : R[X])
(h : is_smul_regular R k) :
(k • p).leading_coeff = k • p.leading_coeff
theorem
polynomial.monic_of_is_unit_leading_coeff_inv_smul
{R : Type u}
[semiring R]
{p : R[X]}
(h : is_unit p.leading_coeff) :