Theory of univariate polynomials

This file starts looking like the ring theory of $ R[X] $

theorem Polynomial.derivative_rootMultiplicity_of_root {R : Type u} [CommRing R] [IsDomain R] [CharZero R] {p : Polynomial R} {t : R} (hpt : Polynomial.IsRoot p t) : Polynomial.rootMultiplicity t (↑Polynomial.derivative p) = Polynomial.rootMultiplicity t p - 1

theorem Polynomial.rootMultiplicity_sub_one_le_derivative_rootMultiplicity {R : Type u} [CommRing R] [IsDomain R] [CharZero R] (p : Polynomial R) (t : R) : Polynomial.rootMultiplicity t p - 1 ≤ Polynomial.rootMultiplicity t (↑Polynomial.derivative p)

instance Polynomial.instNormalizationMonoid {R : Type u} [CommRing R] [IsDomain R] [NormalizationMonoid R] : NormalizationMonoid (Polynomial R)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Polynomial.coe_normUnit {R : Type u} [CommRing R] [IsDomain R] [NormalizationMonoid R] {p : Polynomial R} : ↑(normUnit p) = ↑Polynomial.C ↑(normUnit (Polynomial.leadingCoeff p))

theorem Polynomial.leadingCoeff_normalize {R : Type u} [CommRing R] [IsDomain R] [NormalizationMonoid R] (p : Polynomial R) : Polynomial.leadingCoeff (↑normalize p) = ↑normalize (Polynomial.leadingCoeff p)

theorem Polynomial.Monic.normalize_eq_self {R : Type u} [CommRing R] [IsDomain R] [NormalizationMonoid R] {p : Polynomial R} (hp : Polynomial.Monic p) : ↑normalize p = p

theorem Polynomial.roots_normalize {R : Type u} [CommRing R] [IsDomain R] [NormalizationMonoid R] {p : Polynomial R} : Polynomial.roots (↑normalize p) = Polynomial.roots p

theorem Polynomial.degree_pos_of_ne_zero_of_nonunit {R : Type u} [DivisionRing R] {p : Polynomial R} (hp0 : p ≠ 0) (hp : ¬IsUnit p) : 0 < Polynomial.degree p

theorem Polynomial.monic_mul_leadingCoeff_inv {R : Type u} [DivisionRing R] {p : Polynomial R} (h : p ≠ 0) : Polynomial.Monic (p * ↑Polynomial.C (Polynomial.leadingCoeff p)⁻¹)

theorem Polynomial.degree_mul_leadingCoeff_inv {R : Type u} [DivisionRing R] {q : Polynomial R} (p : Polynomial R) (h : q ≠ 0) : Polynomial.degree (p * ↑Polynomial.C (Polynomial.leadingCoeff q)⁻¹) = Polynomial.degree p

@[simp]

theorem Polynomial.map_eq_zero {R : Type u} {S : Type v} [DivisionRing R] {p : Polynomial R} [Semiring S] [Nontrivial S] (f : R →+* S) : Polynomial.map f p = 0 ↔ p = 0

theorem Polynomial.map_ne_zero {R : Type u} {S : Type v} [DivisionRing R] {p : Polynomial R} [Semiring S] [Nontrivial S] {f : R →+* S} (hp : p ≠ 0) : Polynomial.map f p ≠ 0

@[simp]

theorem Polynomial.degree_map {R : Type u} {S : Type v} [DivisionRing R] [Semiring S] [Nontrivial S] (p : Polynomial R) (f : R →+* S) : Polynomial.degree (Polynomial.map f p) = Polynomial.degree p

@[simp]

theorem Polynomial.natDegree_map {R : Type u} {S : Type v} [DivisionRing R] {p : Polynomial R} [Semiring S] [Nontrivial S] (f : R →+* S) : Polynomial.natDegree (Polynomial.map f p) = Polynomial.natDegree p

@[simp]

theorem Polynomial.leadingCoeff_map {R : Type u} {S : Type v} [DivisionRing R] {p : Polynomial R} [Semiring S] [Nontrivial S] (f : R →+* S) : Polynomial.leadingCoeff (Polynomial.map f p) = ↑f (Polynomial.leadingCoeff p)

theorem Polynomial.monic_map_iff {R : Type u} {S : Type v} [DivisionRing R] [Semiring S] [Nontrivial S] {f : R →+* S} {p : Polynomial R} : Polynomial.Monic (Polynomial.map f p) ↔ Polynomial.Monic p

theorem Polynomial.isUnit_iff_degree_eq_zero {R : Type u} [Field R] {p : Polynomial R} : IsUnit p ↔ Polynomial.degree p = 0

def Polynomial.div {R : Type u} [Field R] (p : Polynomial R) (q : Polynomial R) : (fun x => Polynomial R) (Polynomial.leadingCoeff q)⁻¹

Division of polynomials. See Polynomial.divByMonic for more details.

Equations

• Polynomial.div p q = ↑Polynomial.C (Polynomial.leadingCoeff q)⁻¹ * (p /ₘ (q * ↑Polynomial.C (Polynomial.leadingCoeff q)⁻¹))

def Polynomial.mod {R : Type u} [Field R] (p : Polynomial R) (q : Polynomial R) : Polynomial R

Remainder of polynomial division. See Polynomial.modByMonic for more details.

Equations

• Polynomial.mod p q = p %ₘ (q * ↑Polynomial.C (Polynomial.leadingCoeff q)⁻¹)

instance Polynomial.instDivPolynomialToSemiringToDivisionSemiringToSemifield {R : Type u} [Field R] : Div (Polynomial R)

Equations

• Polynomial.instDivPolynomialToSemiringToDivisionSemiringToSemifield = { div := Polynomial.div }

instance Polynomial.instModPolynomialToSemiringToDivisionSemiringToSemifield {R : Type u} [Field R] : Mod (Polynomial R)

Equations

• Polynomial.instModPolynomialToSemiringToDivisionSemiringToSemifield = { mod := Polynomial.mod }

theorem Polynomial.div_def {R : Type u} [Field R] {p : Polynomial R} {q : Polynomial R} : p / q = ↑Polynomial.C (Polynomial.leadingCoeff q)⁻¹ * (p /ₘ (q * ↑Polynomial.C (Polynomial.leadingCoeff q)⁻¹))

theorem Polynomial.mod_def {R : Type u} [Field R] {p : Polynomial R} {q : Polynomial R} : p % q = p %ₘ (q * ↑Polynomial.C (Polynomial.leadingCoeff q)⁻¹)

theorem Polynomial.modByMonic_eq_mod {R : Type u} [Field R] {q : Polynomial R} (p : Polynomial R) (hq : Polynomial.Monic q) : p %ₘ q = p % q

theorem Polynomial.divByMonic_eq_div {R : Type u} [Field R] {q : Polynomial R} (p : Polynomial R) (hq : Polynomial.Monic q) : p /ₘ q = p / q

theorem Polynomial.mod_X_sub_C_eq_C_eval {R : Type u} [Field R] (p : Polynomial R) (a : R) : p % (Polynomial.X - ↑Polynomial.C a) = ↑Polynomial.C (Polynomial.eval a p)

theorem Polynomial.mul_div_eq_iff_isRoot {R : Type u} {a : R} [Field R] {p : Polynomial R} : (Polynomial.X - ↑Polynomial.C a) * (p / (Polynomial.X - ↑Polynomial.C a)) = p ↔ Polynomial.IsRoot p a

instance Polynomial.instEuclideanDomainPolynomialToSemiringToDivisionSemiringToSemifield {R : Type u} [Field R] : EuclideanDomain (Polynomial R)

Equations

• One or more equations did not get rendered due to their size.

theorem Polynomial.mod_eq_self_iff {R : Type u} [Field R] {p : Polynomial R} {q : Polynomial R} (hq0 : q ≠ 0) : p % q = p ↔ Polynomial.degree p < Polynomial.degree q

theorem Polynomial.div_eq_zero_iff {R : Type u} [Field R] {p : Polynomial R} {q : Polynomial R} (hq0 : q ≠ 0) : p / q = 0 ↔ Polynomial.degree p < Polynomial.degree q

theorem Polynomial.degree_add_div {R : Type u} [Field R] {p : Polynomial R} {q : Polynomial R} (hq0 : q ≠ 0) (hpq : Polynomial.degree q ≤ Polynomial.degree p) : Polynomial.degree q + Polynomial.degree (p / q) = Polynomial.degree p

theorem Polynomial.degree_div_le {R : Type u} [Field R] (p : Polynomial R) (q : Polynomial R) : Polynomial.degree (p / q) ≤ Polynomial.degree p

theorem Polynomial.degree_div_lt {R : Type u} [Field R] {p : Polynomial R} {q : Polynomial R} (hp : p ≠ 0) (hq : 0 < Polynomial.degree q) : Polynomial.degree (p / q) < Polynomial.degree p

theorem Polynomial.isUnit_map {R : Type u} {k : Type y} [Field R] {p : Polynomial R} [Field k] (f : R →+* k) : IsUnit (Polynomial.map f p) ↔ IsUnit p

theorem Polynomial.map_div {R : Type u} {k : Type y} [Field R] {p : Polynomial R} {q : Polynomial R} [Field k] (f : R →+* k) : Polynomial.map f (p / q) = Polynomial.map f p / Polynomial.map f q

theorem Polynomial.map_mod {R : Type u} {k : Type y} [Field R] {p : Polynomial R} {q : Polynomial R} [Field k] (f : R →+* k) : Polynomial.map f (p % q) = Polynomial.map f p % Polynomial.map f q

theorem Polynomial.gcd_map {R : Type u} {k : Type y} [Field R] {p : Polynomial R} {q : Polynomial R} [Field k] [DecidableEq R] [DecidableEq k] (f : R →+* k) : EuclideanDomain.gcd (Polynomial.map f p) (Polynomial.map f q) = Polynomial.map f (EuclideanDomain.gcd p q)

theorem Polynomial.eval₂_gcd_eq_zero {R : Type u} {k : Type y} [Field R] [CommSemiring k] [DecidableEq R] {ϕ : R →+* k} {f : Polynomial R} {g : Polynomial R} {α : k} (hf : Polynomial.eval₂ ϕ α f = 0) (hg : Polynomial.eval₂ ϕ α g = 0) : Polynomial.eval₂ ϕ α (EuclideanDomain.gcd f g) = 0

theorem Polynomial.eval_gcd_eq_zero {R : Type u} [Field R] [DecidableEq R] {f : Polynomial R} {g : Polynomial R} {α : R} (hf : Polynomial.eval α f = 0) (hg : Polynomial.eval α g = 0) : Polynomial.eval α (EuclideanDomain.gcd f g) = 0

theorem Polynomial.root_left_of_root_gcd {R : Type u} {k : Type y} [Field R] [CommSemiring k] [DecidableEq R] {ϕ : R →+* k} {f : Polynomial R} {g : Polynomial R} {α : k} (hα : Polynomial.eval₂ ϕ α (EuclideanDomain.gcd f g) = 0) : Polynomial.eval₂ ϕ α f = 0

theorem Polynomial.root_right_of_root_gcd {R : Type u} {k : Type y} [Field R] [CommSemiring k] [DecidableEq R] {ϕ : R →+* k} {f : Polynomial R} {g : Polynomial R} {α : k} (hα : Polynomial.eval₂ ϕ α (EuclideanDomain.gcd f g) = 0) : Polynomial.eval₂ ϕ α g = 0

theorem Polynomial.root_gcd_iff_root_left_right {R : Type u} {k : Type y} [Field R] [CommSemiring k] [DecidableEq R] {ϕ : R →+* k} {f : Polynomial R} {g : Polynomial R} {α : k} : Polynomial.eval₂ ϕ α (EuclideanDomain.gcd f g) = 0 ↔ Polynomial.eval₂ ϕ α f = 0 ∧ Polynomial.eval₂ ϕ α g = 0

theorem Polynomial.isRoot_gcd_iff_isRoot_left_right {R : Type u} [Field R] [DecidableEq R] {f : Polynomial R} {g : Polynomial R} {α : R} : Polynomial.IsRoot (EuclideanDomain.gcd f g) α ↔ Polynomial.IsRoot f α ∧ Polynomial.IsRoot g α

theorem Polynomial.isCoprime_map {R : Type u} {k : Type y} [Field R] {p : Polynomial R} {q : Polynomial R} [Field k] (f : R →+* k) : IsCoprime (Polynomial.map f p) (Polynomial.map f q) ↔ IsCoprime p q

theorem Polynomial.mem_roots_map {R : Type u} {k : Type y} [Field R] {p : Polynomial R} [CommRing k] [IsDomain k] {f : R →+* k} {x : k} (hp : p ≠ 0) : x ∈ Polynomial.roots (Polynomial.map f p) ↔ Polynomial.eval₂ f x p = 0

theorem Polynomial.rootSet_monomial {R : Type u} {S : Type v} [Field R] [CommRing S] [IsDomain S] [Algebra R S] {n : ℕ} (hn : n ≠ 0) {a : R} (ha : a ≠ 0) : Polynomial.rootSet (↑(Polynomial.monomial n) a) S = {0}

theorem Polynomial.rootSet_C_mul_X_pow {R : Type u} {S : Type v} [Field R] [CommRing S] [IsDomain S] [Algebra R S] {n : ℕ} (hn : n ≠ 0) {a : R} (ha : a ≠ 0) : Polynomial.rootSet (↑Polynomial.C a * Polynomial.X ^ n) S = {0}

theorem Polynomial.rootSet_X_pow {R : Type u} {S : Type v} [Field R] [CommRing S] [IsDomain S] [Algebra R S] {n : ℕ} (hn : n ≠ 0) : Polynomial.rootSet (Polynomial.X ^ n) S = {0}

theorem Polynomial.rootSet_prod {R : Type u} {S : Type v} [Field R] [CommRing S] [IsDomain S] [Algebra R S] {ι : Type u_1} (f : ι → Polynomial R) (s : Finset ι) (h : Finset.prod s f ≠ 0) : Polynomial.rootSet (Finset.prod s f) S = ⋃ (i : ι) (_ : i ∈ s), Polynomial.rootSet (f i) S

theorem Polynomial.exists_root_of_degree_eq_one {R : Type u} [Field R] {p : Polynomial R} (h : Polynomial.degree p = 1) : ∃ x, Polynomial.IsRoot p x

theorem Polynomial.coeff_inv_units {R : Type u} [Field R] (u : (Polynomial R)ˣ) (n : ℕ) : (Polynomial.coeff (↑u) n)⁻¹ = Polynomial.coeff (↑u⁻¹) n

theorem Polynomial.monic_normalize {R : Type u} [Field R] {p : Polynomial R} [DecidableEq R] (hp0 : p ≠ 0) : Polynomial.Monic (↑normalize p)

theorem Polynomial.leadingCoeff_div {R : Type u} [Field R] {p : Polynomial R} {q : Polynomial R} (hpq : Polynomial.degree q ≤ Polynomial.degree p) : Polynomial.leadingCoeff (p / q) = Polynomial.leadingCoeff p / Polynomial.leadingCoeff q

theorem Polynomial.div_C_mul {R : Type u} {a : R} [Field R] {p : Polynomial R} {q : Polynomial R} : p / (↑Polynomial.C a * q) = ↑Polynomial.C a⁻¹ * (p / q)

theorem Polynomial.C_mul_dvd {R : Type u} {a : R} [Field R] {p : Polynomial R} {q : Polynomial R} (ha : a ≠ 0) : ↑Polynomial.C a * p ∣ q ↔ p ∣ q

theorem Polynomial.dvd_C_mul {R : Type u} {a : R} [Field R] {p : Polynomial R} {q : Polynomial R} (ha : a ≠ 0) : p ∣ ↑Polynomial.C a * q ↔ p ∣ q

theorem Polynomial.coe_normUnit_of_ne_zero {R : Type u} [Field R] {p : Polynomial R} [DecidableEq R] (hp : p ≠ 0) : ↑(normUnit p) = ↑Polynomial.C (Polynomial.leadingCoeff p)⁻¹

theorem Polynomial.normalize_monic {R : Type u} [Field R] {p : Polynomial R} [DecidableEq R] (h : Polynomial.Monic p) : ↑normalize p = p

theorem Polynomial.map_dvd_map' {R : Type u} {k : Type y} [Field R] [Field k] (f : R →+* k) {x : Polynomial R} {y : Polynomial R} : Polynomial.map f x ∣ Polynomial.map f y ↔ x ∣ y

theorem Polynomial.degree_normalize {R : Type u} [Field R] {p : Polynomial R} [DecidableEq R] : Polynomial.degree (↑normalize p) = Polynomial.degree p

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

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

theorem Polynomial.not_irreducible_C {R : Type u} [Field R] (x : R) : ¬Irreducible (↑Polynomial.C x)

theorem Polynomial.degree_pos_of_irreducible {R : Type u} [Field R] {p : Polynomial R} (hp : Irreducible p) : 0 < Polynomial.degree p

theorem Polynomial.X_sub_C_mul_divByMonic_eq_sub_modByMonic {K : Type u_1} [Field K] (f : Polynomial K) (a : K) : (Polynomial.X - ↑Polynomial.C a) * (f /ₘ (Polynomial.X - ↑Polynomial.C a)) = f - f %ₘ (Polynomial.X - ↑Polynomial.C a)

theorem Polynomial.divByMonic_add_X_sub_C_mul_derivate_divByMonic_eq_derivative {K : Type u_1} [Field K] (f : Polynomial K) (a : K) : f /ₘ (Polynomial.X - ↑Polynomial.C a) + (Polynomial.X - ↑Polynomial.C a) * ↑Polynomial.derivative (f /ₘ (Polynomial.X - ↑Polynomial.C a)) = ↑Polynomial.derivative f

theorem Polynomial.X_sub_C_dvd_derivative_of_X_sub_C_dvd_divByMonic {K : Type u_1} [Field K] (f : Polynomial K) {a : K} (hf : Polynomial.X - ↑Polynomial.C a ∣ f /ₘ (Polynomial.X - ↑Polynomial.C a)) : Polynomial.X - ↑Polynomial.C a ∣ ↑Polynomial.derivative f

theorem Polynomial.isCoprime_of_is_root_of_eval_derivative_ne_zero {K : Type u_1} [Field K] (f : Polynomial K) (a : K) (hf' : Polynomial.eval a (↑Polynomial.derivative f) ≠ 0) : IsCoprime (Polynomial.X - ↑Polynomial.C a) (f /ₘ (Polynomial.X - ↑Polynomial.C a))

If f is a polynomial over a field, and a : K satisfies f' a ≠ 0, then f / (X - a) is coprime with X - a. Note that we do not assume f a = 0, because f / (X - a) = (f - f a) / (X - a).