Documentation

Mathlib.Data.Polynomial.FieldDivision

Theory of univariate polynomials #

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

theorem Polynomial.rootMultiplicity_sub_one_le_derivative_rootMultiplicity_of_ne_zero {R : Type u} [CommRing R] (p : Polynomial R) (t : R) (hnezero : Polynomial.derivative p 0) :
theorem Polynomial.isRoot_iterate_derivative_of_lt_rootMultiplicity {R : Type u} [CommRing R] {p : Polynomial R} {t : R} {n : } (hn : n < Polynomial.rootMultiplicity t p) :
Polynomial.IsRoot ((Polynomial.derivative)^[n] p) t
theorem Polynomial.lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors {R : Type u} [CommRing R] {p : Polynomial R} {t : R} {n : } (h : p 0) (hroot : mn, Polynomial.IsRoot ((Polynomial.derivative)^[m] p) t) (hnzd : (Nat.factorial n) nonZeroDivisors R) :
theorem Polynomial.lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors' {R : Type u} [CommRing R] {p : Polynomial R} {t : R} {n : } (h : p 0) (hroot : mn, Polynomial.IsRoot ((Polynomial.derivative)^[m] p) t) (hnzd : mn, m 0m nonZeroDivisors R) :
theorem Polynomial.lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors {R : Type u} [CommRing R] {p : Polynomial R} {t : R} {n : } (h : p 0) (hnzd : (Nat.factorial n) nonZeroDivisors R) :
n < Polynomial.rootMultiplicity t p mn, Polynomial.IsRoot ((Polynomial.derivative)^[m] p) t
theorem Polynomial.lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors' {R : Type u} [CommRing R] {p : Polynomial R} {t : R} {n : } (h : p 0) (hnzd : mn, m 0m nonZeroDivisors R) :
n < Polynomial.rootMultiplicity t p mn, Polynomial.IsRoot ((Polynomial.derivative)^[m] p) t
theorem Polynomial.one_lt_rootMultiplicity_iff_isRoot_iterate_derivative {R : Type u} [CommRing R] {p : Polynomial R} {t : R} (h : p 0) :
1 < Polynomial.rootMultiplicity t p m1, Polynomial.IsRoot ((Polynomial.derivative)^[m] p) t
theorem Polynomial.one_lt_rootMultiplicity_iff_isRoot_gcd {R : Type u} [CommRing R] [IsDomain R] [GCDMonoid (Polynomial R)] {p : Polynomial R} {t : R} (h : p 0) :
1 < Polynomial.rootMultiplicity t p Polynomial.IsRoot (gcd p (Polynomial.derivative p)) t
theorem Polynomial.lt_rootMultiplicity_of_isRoot_iterate_derivative {R : Type u} [CommRing R] [IsDomain R] [CharZero R] {p : Polynomial R} {t : R} {n : } (h : p 0) (hroot : mn, Polynomial.IsRoot ((Polynomial.derivative)^[m] p) t) :
theorem Polynomial.lt_rootMultiplicity_iff_isRoot_iterate_derivative {R : Type u} [CommRing R] [IsDomain R] [CharZero R] {p : Polynomial R} {t : R} {n : } (h : p 0) :
n < Polynomial.rootMultiplicity t p mn, Polynomial.IsRoot ((Polynomial.derivative)^[m] p) t
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))
@[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) :
def Polynomial.div {R : Type u} [Field R] (p : Polynomial R) (q : Polynomial R) :

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

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

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

    Equations
    Instances For
      Equations
      • Polynomial.instDivPolynomialToSemiringToDivisionSemiringToSemifield = { div := Polynomial.div }
      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
      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) :
      theorem Polynomial.div_eq_zero_iff {R : Type u} [Field R] {p : Polynomial R} {q : Polynomial R} (hq0 : q 0) :
      theorem Polynomial.degree_div_lt {R : Type u} [Field R] {p : Polynomial R} {q : Polynomial R} (hp : p 0) (hq : 0 < Polynomial.degree q) :
      theorem Polynomial.isUnit_map {R : Type u} {k : Type y} [Field R] {p : Polynomial R} [Field k] (f : R →+* k) :
      theorem Polynomial.map_div {R : Type u} {k : Type y} [Field R] {p : Polynomial R} {q : Polynomial R} [Field k] (f : R →+* k) :
      theorem Polynomial.map_mod {R : Type u} {k : Type y} [Field R] {p : Polynomial R} {q : Polynomial R} [Field k] (f : R →+* k) :
      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) :
      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) :
      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) :
      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) :
      theorem Polynomial.isCoprime_map {R : Type u} {k : Type y} [Field R] {p : Polynomial R} {q : Polynomial R} [Field k] (f : R →+* k) :
      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) :
      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) :
      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 ∈ s, Polynomial.rootSet (f i) S
      theorem Polynomial.monic_normalize {R : Type u} [Field R] {p : Polynomial R} [DecidableEq R] (hp0 : p 0) :
      Polynomial.Monic (normalize p)
      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} :
      theorem Polynomial.not_irreducible_C {R : Type u} [Field R] (x : R) :
      ¬Irreducible (Polynomial.C x)
      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).

      theorem Polynomial.irreducible_iff_degree_lt {R : Type u} [Field R] (p : Polynomial R) (hp0 : p 0) (hpu : ¬IsUnit p) :

      To check a polynomial over a field is irreducible, it suffices to check only for divisors that have smaller degree.

      See also: Polynomial.Monic.irreducible_iff_natDegree.

      To check a polynomial p over a field is irreducible, it suffices to check there are no divisors of degree 0 < d ≤ degree p / 2.

      See also: Polynomial.Monic.irreducible_iff_natDegree'.

      An irreducible polynomial over a field must have positive degree.