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_zero_iff_subsingleton'
{R : Type u}
[Semiring R]
:
Polynomial.Monic 0 ↔ (∀ (f g : Polynomial R), f = g) ∧ ∀ (a b : R), a = b
theorem
Polynomial.ne_zero_of_ne_zero_of_monic
{R : Type u}
[Semiring R]
{p : Polynomial R}
{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_leadingCoeff_eq_one
{R : Type u}
[Semiring R]
{p : Polynomial R}
{b : R}
(hp : b * p.leadingCoeff = 1)
:
(Polynomial.C b * p).Monic
theorem
Polynomial.monic_mul_C_of_leadingCoeff_mul_eq_one
{R : Type u}
[Semiring R]
{p : Polynomial R}
{b : R}
(hp : p.leadingCoeff * b = 1)
:
(p * Polynomial.C b).Monic
theorem
Polynomial.monic_of_degree_le
{R : Type u}
[Semiring R]
{p : Polynomial R}
(n : ℕ)
(H1 : p.degree ≤ ↑n)
(H2 : p.coeff n = 1)
:
p.Monic
theorem
Polynomial.monic_X_pow_add
{R : Type u}
[Semiring R]
{p : Polynomial R}
{n : ℕ}
(H : p.degree < ↑n)
:
theorem
Polynomial.monic_X_add_C
{R : Type u}
[Semiring R]
(x : R)
:
(Polynomial.X + Polynomial.C x).Monic
theorem
Polynomial.Monic.mul
{R : Type u}
[Semiring R]
{p : Polynomial R}
{q : Polynomial R}
(hp : p.Monic)
(hq : q.Monic)
:
(p * q).Monic
theorem
Polynomial.Monic.pow
{R : Type u}
[Semiring R]
{p : Polynomial R}
(hp : p.Monic)
(n : ℕ)
:
(p ^ n).Monic
theorem
Polynomial.Monic.add_of_left
{R : Type u}
[Semiring R]
{p : Polynomial R}
{q : Polynomial R}
(hp : p.Monic)
(hpq : q.degree < p.degree)
:
(p + q).Monic
theorem
Polynomial.Monic.add_of_right
{R : Type u}
[Semiring R]
{p : Polynomial R}
{q : Polynomial R}
(hq : q.Monic)
(hpq : p.degree < q.degree)
:
(p + q).Monic
theorem
Polynomial.Monic.of_mul_monic_left
{R : Type u}
[Semiring R]
{p : Polynomial R}
{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 : Polynomial R}
{q : Polynomial R}
(hq : q.Monic)
(hpq : (p * q).Monic)
:
p.Monic
@[simp]
theorem
Polynomial.Monic.natDegree_eq_zero_iff_eq_one
{R : Type u}
[Semiring R]
{p : Polynomial R}
(hp : p.Monic)
:
@[simp]
theorem
Polynomial.Monic.degree_le_zero_iff_eq_one
{R : Type u}
[Semiring R]
{p : Polynomial R}
(hp : p.Monic)
:
theorem
Polynomial.Monic.natDegree_mul
{R : Type u}
[Semiring R]
{p : Polynomial R}
{q : Polynomial R}
(hp : p.Monic)
(hq : q.Monic)
:
theorem
Polynomial.Monic.degree_mul_comm
{R : Type u}
[Semiring R]
{p : Polynomial R}
(hp : p.Monic)
(q : Polynomial R)
:
theorem
Polynomial.Monic.natDegree_mul'
{R : Type u}
[Semiring R]
{p : Polynomial R}
{q : Polynomial R}
(hp : p.Monic)
(hq : q ≠ 0)
:
theorem
Polynomial.Monic.natDegree_mul_comm
{R : Type u}
[Semiring R]
{p : Polynomial R}
(hp : p.Monic)
(q : Polynomial R)
:
theorem
Polynomial.Monic.not_dvd_of_natDegree_lt
{R : Type u}
[Semiring R]
{p : Polynomial R}
{q : Polynomial R}
(hp : p.Monic)
(h0 : q ≠ 0)
(hl : q.natDegree < p.natDegree)
:
theorem
Polynomial.Monic.not_dvd_of_degree_lt
{R : Type u}
[Semiring R]
{p : Polynomial R}
{q : Polynomial R}
(hp : p.Monic)
(h0 : q ≠ 0)
(hl : q.degree < p.degree)
:
theorem
Polynomial.Monic.nextCoeff_mul
{R : Type u}
[Semiring R]
{p : Polynomial R}
{q : Polynomial R}
(hp : p.Monic)
(hq : q.Monic)
:
theorem
Polynomial.Monic.nextCoeff_pow
{R : Type u}
[Semiring R]
{p : Polynomial R}
(hp : p.Monic)
(n : ℕ)
:
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.natDegree_pow
{R : Type u}
[Semiring R]
{p : Polynomial R}
(hp : p.Monic)
(n : ℕ)
:
@[simp]
theorem
Polynomial.Monic.eq_one_of_isUnit
{R : Type u}
[Semiring R]
{p : Polynomial R}
(hm : p.Monic)
(hpu : IsUnit p)
:
p = 1
theorem
Polynomial.eq_of_monic_of_associated
{R : Type u}
[Semiring R]
{p : Polynomial R}
{q : Polynomial R}
(hp : p.Monic)
(hq : q.Monic)
(hpq : Associated p q)
:
p = q
theorem
Polynomial.monic_multiset_prod_of_monic
{R : Type u}
{ι : Type y}
[CommSemiring R]
(t : Multiset ι)
(f : ι → Polynomial R)
(ht : ∀ i ∈ t, (f i).Monic)
:
(Multiset.map f t).prod.Monic
theorem
Polynomial.monic_prod_of_monic
{R : Type u}
{ι : Type y}
[CommSemiring R]
(s : Finset ι)
(f : ι → Polynomial R)
(hs : ∀ i ∈ s, (f i).Monic)
:
(∏ i ∈ s, f i).Monic
theorem
Polynomial.Monic.nextCoeff_multiset_prod
{R : Type u}
{ι : Type y}
[CommSemiring R]
(t : Multiset ι)
(f : ι → Polynomial R)
(h : ∀ i ∈ t, (f i).Monic)
:
(Multiset.map f t).prod.nextCoeff = (Multiset.map (fun (i : ι) => (f i).nextCoeff) t).sum
theorem
Polynomial.Monic.nextCoeff_prod
{R : Type u}
{ι : Type y}
[CommSemiring R]
(s : Finset ι)
(f : ι → Polynomial R)
(h : ∀ i ∈ s, (f i).Monic)
:
(∏ i ∈ s, f i).nextCoeff = ∑ i ∈ s, (f i).nextCoeff
@[simp]
theorem
Polynomial.Monic.natDegree_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).natDegree = P.natDegree
@[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.natDegree_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).natDegree = p.natDegree
theorem
Polynomial.leadingCoeff_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).leadingCoeff = f p.leadingCoeff
theorem
Polynomial.nextCoeff_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).nextCoeff = f p.nextCoeff
theorem
Polynomial.leadingCoeff_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).leadingCoeff = f p.leadingCoeff
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_sub_C
{R : Type u}
[Ring R]
(x : R)
:
(Polynomial.X - Polynomial.C x).Monic
theorem
Polynomial.monic_X_pow_sub
{R : Type u}
[Ring R]
{p : Polynomial R}
{n : ℕ}
(H : p.degree < ↑n)
:
theorem
Polynomial.Monic.sub_of_left
{R : Type u}
[Ring R]
{p : Polynomial R}
{q : Polynomial R}
(hp : p.Monic)
(hpq : q.degree < p.degree)
:
(p - q).Monic
theorem
Polynomial.Monic.sub_of_right
{R : Type u}
[Ring R]
{p : Polynomial R}
{q : Polynomial R}
(hq : q.leadingCoeff = -1)
(hpq : p.degree < q.degree)
:
(p - q).Monic
@[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_natDegree_lt_iff
{R : Type u}
[Semiring R]
{p : Polynomial R}
(h : p.Monic)
{q : Polynomial R}
:
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]
[DistribMulAction S R]
{k : S}
(p : Polynomial R)
(h : IsSMulRegular R k)
:
theorem
Polynomial.natDegree_smul_of_smul_regular
{R : Type u}
[Semiring R]
{S : Type u_1}
[Monoid S]
[DistribMulAction S R]
{k : S}
(p : Polynomial R)
(h : IsSMulRegular R k)
:
theorem
Polynomial.leadingCoeff_smul_of_smul_regular
{R : Type u}
[Semiring R]
{S : Type u_1}
[Monoid S]
[DistribMulAction S R]
{k : S}
(p : Polynomial R)
(h : IsSMulRegular R k)
:
theorem
Polynomial.monic_of_isUnit_leadingCoeff_inv_smul
{R : Type u}
[Semiring R]
{p : Polynomial R}
(h : IsUnit p.leadingCoeff)
:
theorem
Polynomial.isUnit_leadingCoeff_mul_right_eq_zero_iff
{R : Type u}
[Semiring R]
{p : Polynomial R}
(h : IsUnit p.leadingCoeff)
{q : Polynomial R}
:
theorem
Polynomial.isUnit_leadingCoeff_mul_left_eq_zero_iff
{R : Type u}
[Semiring R]
{p : Polynomial R}
(h : IsUnit p.leadingCoeff)
{q : Polynomial R}
: