Theory of monic polynomials #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 : polynomial R}
(hp : 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.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_C_mul_of_mul_leading_coeff_eq_one
{R : Type u}
[semiring R]
{p : polynomial R}
{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 : polynomial 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.of_mul_monic_left
{R : Type u}
[semiring R]
{p q : polynomial R}
(hp : p.monic)
(hpq : (p * q).monic) :
q.monic
theorem
polynomial.monic.of_mul_monic_right
{R : Type u}
[semiring R]
{p q : polynomial R}
(hq : q.monic)
(hpq : (p * q).monic) :
p.monic
@[simp]
theorem
polynomial.monic.nat_degree_eq_zero_iff_eq_one
{R : Type u}
[semiring R]
{p : polynomial R}
(hp : p.monic) :
p.nat_degree = 0 ↔ p = 1
@[simp]
theorem
polynomial.monic.degree_le_zero_iff_eq_one
{R : Type u}
[semiring R]
{p : polynomial R}
(hp : p.monic) :
theorem
polynomial.monic.nat_degree_mul
{R : Type u}
[semiring R]
{p q : polynomial R}
(hp : p.monic)
(hq : q.monic) :
(p * q).nat_degree = p.nat_degree + q.nat_degree
theorem
polynomial.monic.degree_mul_comm
{R : Type u}
[semiring R]
{p : polynomial R}
(hp : p.monic)
(q : polynomial R) :
theorem
polynomial.monic.nat_degree_mul'
{R : Type u}
[semiring R]
{p q : polynomial R}
(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 : polynomial R}
(hp : p.monic)
(q : polynomial R) :
(p * q).nat_degree = (q * p).nat_degree
theorem
polynomial.monic.not_dvd_of_nat_degree_lt
{R : Type u}
[semiring R]
{p q : polynomial R}
(hp : p.monic)
(h0 : q ≠ 0)
(hl : q.nat_degree < p.nat_degree) :
theorem
polynomial.monic.next_coeff_mul
{R : Type u}
[semiring R]
{p q : polynomial R}
(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 : polynomial R}
{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 : polynomial R}
(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.eq_one_of_is_unit
{R : Type u}
[semiring R]
{p : polynomial R}
(hm : p.monic)
(hpu : is_unit p) :
p = 1
theorem
polynomial.monic_multiset_prod_of_monic
{R : Type u}
{ι : Type y}
[comm_semiring R]
(t : multiset ι)
(f : ι → polynomial R)
(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 : ι → polynomial R)
(hs : ∀ (i : ι), i ∈ s → (f i).monic) :
theorem
polynomial.monic.next_coeff_multiset_prod
{R : Type u}
{ι : Type y}
[comm_semiring R]
(t : multiset ι)
(f : ι → polynomial R)
(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 : ι → polynomial R)
(h : ∀ (i : ι), i ∈ s → (f i).monic) :
(s.prod (λ (i : ι), f i)).next_coeff = s.sum (λ (i : ι), (f i).next_coeff)
@[simp]
theorem
polynomial.monic.nat_degree_map
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
[nontrivial S]
{P : polynomial R}
(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 : polynomial R}
(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 : polynomial R) :
(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 : 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
theorem
polynomial.next_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).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 : polynomial R) :
(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 : polynomial R}
(hp : (polynomial.map f p).monic) :
p.monic
theorem
function.injective.monic_map_iff
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
{f : R →+* S}
(hf : function.injective ⇑f)
{p : polynomial R} :
p.monic ↔ (polynomial.map f p).monic
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.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)
theorem
polynomial.monic.sub_of_right
{R : Type u}
[ring R]
{p q : polynomial R}
(hq : q.leading_coeff = -1)
(hpq : p.degree < q.degree) :
@[simp]
theorem
polynomial.monic.mul_left_ne_zero
{R : Type u}
[semiring R]
{p : polynomial R}
(hp : p.monic)
{q : polynomial R}
(hq : q ≠ 0) :
theorem
polynomial.monic.mul_right_ne_zero
{R : Type u}
[semiring R]
{p : polynomial R}
(hp : p.monic)
{q : polynomial R}
(hq : q ≠ 0) :
theorem
polynomial.monic.mul_nat_degree_lt_iff
{R : Type u}
[semiring R]
{p : polynomial R}
(h : p.monic)
{q : polynomial R} :
(p * q).nat_degree < p.nat_degree ↔ p ≠ 1 ∧ q = 0
theorem
polynomial.monic.mul_right_eq_zero_iff
{R : Type u}
[semiring R]
{p : polynomial R}
(h : p.monic)
{q : polynomial R} :
theorem
polynomial.monic.mul_left_eq_zero_iff
{R : Type u}
[semiring R]
{p : polynomial R}
(h : p.monic)
{q : polynomial R} :
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 : polynomial R)
(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 : polynomial R)
(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 : polynomial R)
(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 : polynomial R}
(h : is_unit p.leading_coeff) :
theorem
polynomial.is_unit_leading_coeff_mul_right_eq_zero_iff
{R : Type u}
[semiring R]
{p : polynomial R}
(h : is_unit p.leading_coeff)
{q : polynomial R} :
theorem
polynomial.is_unit_leading_coeff_mul_left_eq_zero_iff
{R : Type u}
[semiring R]
{p : polynomial R}
(h : is_unit p.leading_coeff)
{q : polynomial R} :