Theory of univariate polynomials

We prove basic results about univariate polynomials.

theorem Polynomial.natDegree_pos_of_aeval_root {R : Type u} {S : Type v} [CommRing R] [Semiring S] [Algebra R S] {p : Polynomial R} (hp : p ≠ 0) {z : S} (hz : (aeval z) p = 0) (inj : ∀ (x : R), (algebraMap R S) x = 0 → x = 0) : 0 < p.natDegree

theorem Polynomial.degree_pos_of_aeval_root {R : Type u} {S : Type v} [CommRing R] [Semiring S] [Algebra R S] {p : Polynomial R} (hp : p ≠ 0) {z : S} (hz : (aeval z) p = 0) (inj : ∀ (x : R), (algebraMap R S) x = 0 → x = 0) : 0 < p.degree

theorem Polynomial.smul_divByMonic {R : Type u} [CommRing R] {q : Polynomial R} (c : R) (p : Polynomial R) : c • p /ₘ q = c • (p /ₘ q)

theorem Polynomial.smul_modByMonic {R : Type u} [CommRing R] {q : Polynomial R} (c : R) (p : Polynomial R) : c • p %ₘ q = c • (p %ₘ q)

noncomputable def Polynomial.divByMonicHom {R : Type u} [CommRing R] (q : Polynomial R) : Polynomial R →ₗ[R] Polynomial R

_ /ₘ q as an R-linear map.

Equations

• q.divByMonicHom = { toFun := fun (p : Polynomial R) => p /ₘ q, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Polynomial.divByMonicHom_apply {R : Type u} [CommRing R] (q p : Polynomial R) : q.divByMonicHom p = p /ₘ q

theorem Polynomial.mem_ker_divByMonic {R : Type u} [CommRing R] {q : Polynomial R} [Nontrivial R] (hq : q.Monic) {p : Polynomial R} : p ∈ q.divByMonicHom.ker ↔ p.degree < q.degree

noncomputable def Polynomial.modByMonicHom {R : Type u} [CommRing R] (q : Polynomial R) : Polynomial R →ₗ[R] Polynomial R

_ %ₘ q as an R-linear map.

Equations

• q.modByMonicHom = { toFun := fun (p : Polynomial R) => p %ₘ q, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Polynomial.modByMonicHom_apply {R : Type u} [CommRing R] (q p : Polynomial R) : q.modByMonicHom p = p %ₘ q

theorem Polynomial.mem_ker_modByMonic {R : Type u} [CommRing R] {q : Polynomial R} (hq : q.Monic) {p : Polynomial R} : p ∈ q.modByMonicHom.ker ↔ q ∣ p

theorem Polynomial.aeval_modByMonic_eq_self_of_root {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {p q : Polynomial R} {x : S} (hx : (aeval x) q = 0) : (aeval x) (p %ₘ q) = (aeval x) p

theorem Polynomial.trailingDegree_mul {R : Type u} [Semiring R] [NoZeroDivisors R] {p q : Polynomial R} : (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

theorem Polynomial.rootMultiplicity_eq_rootMultiplicity {R : Type u} [CommRing R] {p : Polynomial R} {t : R} : rootMultiplicity t p = rootMultiplicity 0 (p.comp (X + C t))

theorem Polynomial.rootMultiplicity_eq_natTrailingDegree {R : Type u} [CommRing R] {p : Polynomial R} {t : R} : rootMultiplicity t p = (p.comp (X + C t)).natTrailingDegree

See Polynomial.rootMultiplicity_eq_natTrailingDegree' for the special case of t = 0.

theorem Polynomial.Monic.mem_nonZeroDivisors {R : Type u} [CommRing R] {p : Polynomial R} (h : p.Monic) : p ∈ nonZeroDivisors (Polynomial R)

theorem Polynomial.mem_nonZeroDivisors_of_leadingCoeff {R : Type u} [CommRing R] {p : Polynomial R} (h : p.leadingCoeff ∈ nonZeroDivisors R) : p ∈ nonZeroDivisors (Polynomial R)

theorem Polynomial.mem_nonZeroDivisors_of_trailingCoeff {R : Type u} [CommRing R] {p : Polynomial R} (h : p.trailingCoeff ∈ nonZeroDivisors R) : p ∈ nonZeroDivisors (Polynomial R)

theorem Irreducible.aeval_ne_zero_of_natDegree_ne_one {R : Type u} {S : Type v} [CommRing R] [IsDomain R] [Ring S] [Algebra R S] [FaithfulSMul R S] {p : Polynomial R} (hp : Irreducible p) (hdeg : p.natDegree ≠ 1) {x : S} (hx : x ∈ (algebraMap R S).range) : (Polynomial.aeval x) p ≠ 0

theorem Polynomial.natDegree_pos_of_monic_of_aeval_eq_zero {R : Type u} {S : Type v} [CommRing R] [Nontrivial R] [Semiring S] [Algebra R S] [FaithfulSMul R S] {p : Polynomial R} (hp : p.Monic) {x : S} (hx : (aeval x) p = 0) : 0 < p.natDegree

theorem Polynomial.rootMultiplicity_mul_X_sub_C_pow {R : Type u} [CommRing R] {p : Polynomial R} {a : R} {n : ℕ} (h : p ≠ 0) : rootMultiplicity a (p * (X - C a) ^ n) = rootMultiplicity a p + n

theorem Polynomial.rootMultiplicity_X_sub_C_pow {R : Type u} [CommRing R] [Nontrivial R] (a : R) (n : ℕ) : rootMultiplicity a ((X - C a) ^ n) = n

The multiplicity of a as root of (X - a) ^ n is n.

theorem Polynomial.rootMultiplicity_X_sub_C_self {R : Type u} [CommRing R] [Nontrivial R] {x : R} : rootMultiplicity x (X - C x) = 1

theorem Polynomial.rootMultiplicity_X_sub_C {R : Type u} [CommRing R] [Nontrivial R] [DecidableEq R] {x y : R} : rootMultiplicity x (X - C y) = if x = y then 1 else 0

theorem Polynomial.rootMultiplicity_comp_C_mul_X_add_C {R : Type u} [CommRing R] (p : Polynomial R) (a b c : R) (ha : IsUnit a) : rootMultiplicity c (p.comp (C a * X + C b)) = rootMultiplicity (a * c + b) p

theorem Polynomial.rootMultiplicity_mul' {R : Type u} [CommRing R] {p q : Polynomial R} {x : R} (hpq : eval x (p /ₘ (X - C x) ^ rootMultiplicity x p) * eval x (q /ₘ (X - C x) ^ rootMultiplicity x q) ≠ 0) : rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q

theorem Polynomial.Monic.neg_one_pow_natDegree_mul_comp_neg_X {R : Type u} [CommRing R] {p : Polynomial R} (hp : p.Monic) : ((-1) ^ p.natDegree * p.comp (-X)).Monic

theorem Polynomial.degree_eq_degree_of_associated {R : Type u} [CommRing R] [IsDomain R] {p q : Polynomial R} (h : Associated p q) : p.degree = q.degree

theorem Polynomial.prime_X_sub_C {R : Type u} [CommRing R] [IsDomain R] (r : R) : Prime (X - C r)

theorem Polynomial.prime_X {R : Type u} [CommRing R] [IsDomain R] : Prime X

theorem Polynomial.Monic.prime_of_degree_eq_one {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hp1 : p.degree = 1) (hm : p.Monic) : Prime p

theorem Polynomial.irreducible_X_sub_C {R : Type u} [CommRing R] [IsDomain R] (r : R) : Irreducible (X - C r)

theorem Polynomial.irreducible_X {R : Type u} [CommRing R] [IsDomain R] : Irreducible X

theorem Polynomial.Monic.irreducible_of_degree_eq_one {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hp1 : p.degree = 1) (hm : p.Monic) : Irreducible p

theorem Polynomial.irreducible_of_degree_eq_one_of_isRelPrime_coeff {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hp : p.degree = 1) (hc : IsRelPrime (p.coeff 0) (p.coeff 1)) : Irreducible p

A degree 1 polynomial C a * X + C b is irreducible if a, b are relatively prime.

theorem Polynomial.irreducible_C_mul_X_add_C {R : Type u} [CommRing R] [IsDomain R] {a b : R} (ha : a ≠ 0) (hab : IsRelPrime a b) : Irreducible (C a * X + C b)

theorem Polynomial.aeval_ne_zero_of_isCoprime {S : Type v} {R : Type u_1} [CommSemiring R] [Nontrivial S] [Semiring S] [Algebra R S] {p q : Polynomial R} (h : IsCoprime p q) (s : S) : (aeval s) p ≠ 0 ∨ (aeval s) q ≠ 0

theorem Polynomial.isCoprime_X_sub_C_of_isUnit_sub {R : Type u_1} [CommRing R] {a b : R} (h : IsUnit (a - b)) : IsCoprime (X - C a) (X - C b)

theorem Polynomial.pairwise_coprime_X_sub_C {K : Type u_1} [Field K] {I : Type v} {s : I → K} (H : Function.Injective s) : Pairwise (Function.onFun IsCoprime fun (i : I) => X - C (s i))

theorem Polynomial.rootMultiplicity_mul {R : Type u} [CommRing R] [IsDomain R] {p q : Polynomial R} {x : R} (hpq : p * q ≠ 0) : rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q

theorem Polynomial.exists_multiset_roots {R : Type u} [CommRing R] [IsDomain R] [DecidableEq R] {p : Polynomial R} : p ≠ 0 → ∃ (s : Multiset R), ↑s.card ≤ p.degree ∧ ∀ (a : R), Multiset.count a s = rootMultiplicity a p