Documentation

Mathlib.Data.Polynomial.RingDivision

Theory of univariate polynomials #

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

Main definitions #

Main statements #

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 : ↑(Polynomial.aeval z) p = 0) (inj : ∀ (x : R), ↑(algebraMap R S) x = 0x = 0) :
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 : ↑(Polynomial.aeval z) p = 0) (inj : ∀ (x : R), ↑(algebraMap R S) x = 0x = 0) :
theorem Polynomial.modByMonic_eq_of_dvd_sub {R : Type u} [CommRing R] {q : Polynomial R} (hq : Polynomial.Monic q) {p₁ : Polynomial R} {p₂ : Polynomial R} (h : q p₁ - p₂) :
p₁ %ₘ q = p₂ %ₘ q
theorem Polynomial.add_modByMonic {R : Type u} [CommRing R] {q : Polynomial R} (p₁ : Polynomial R) (p₂ : Polynomial R) :
(p₁ + p₂) %ₘ q = p₁ %ₘ q + 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)
@[simp]

_ %ₘ q as an R-linear map.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem Polynomial.aeval_modByMonic_eq_self_of_root {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {p : Polynomial R} {q : Polynomial R} (hq : Polynomial.Monic q) {x : S} (hx : ↑(Polynomial.aeval x) q = 0) :
    ↑(Polynomial.aeval x) (p %ₘ q) = ↑(Polynomial.aeval x) p
    theorem Polynomial.natDegree_sub_eq_of_prod_eq {R : Type u} [Semiring R] [NoZeroDivisors R] {p₁ : Polynomial R} {p₂ : Polynomial R} {q₁ : Polynomial R} {q₂ : Polynomial R} (hp₁ : p₁ 0) (hq₁ : q₁ 0) (hp₂ : p₂ 0) (hq₂ : q₂ 0) (h_eq : p₁ * q₂ = p₂ * q₁) :

    This lemma is useful for working with the intDegree of a rational function.

    theorem Polynomial.isUnit_iff {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} :
    IsUnit p r, IsUnit r Polynomial.C r = p

    Characterization of a unit of a polynomial ring over an integral domain R. See Polynomial.isUnit_iff_coeff_isUnit_isNilpotent when R is a commutative ring.

    theorem Polynomial.irreducible_of_monic {R : Type u} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} (hp : Polynomial.Monic p) (hp1 : p 1) :
    Irreducible p ∀ (f g : Polynomial R), Polynomial.Monic fPolynomial.Monic gf * g = pf = 1 g = 1
    theorem Polynomial.le_rootMultiplicity_iff {R : Type u} [CommRing R] {p : Polynomial R} (p0 : p 0) {a : R} {n : } :
    n Polynomial.rootMultiplicity a p (Polynomial.X - Polynomial.C a) ^ n p

    The multiplicity of a as root of a nonzero polynomial p is at least n iff (X - a) ^ n divides p.

    theorem Polynomial.rootMultiplicity_le_iff {R : Type u} [CommRing R] {p : Polynomial R} (p0 : p 0) (a : R) (n : ) :
    Polynomial.rootMultiplicity a p n ¬(Polynomial.X - Polynomial.C a) ^ (n + 1) p
    theorem Polynomial.pow_rootMultiplicity_not_dvd {R : Type u} [CommRing R] {p : Polynomial R} (p0 : p 0) (a : R) :
    ¬(Polynomial.X - Polynomial.C a) ^ (Polynomial.rootMultiplicity a p + 1) p

    The multiplicity of p + q is at least the minimum of the multiplicities.

    theorem Polynomial.prime_X_sub_C {R : Type u} [CommRing R] [IsDomain R] (r : R) :
    Prime (Polynomial.X - Polynomial.C r)
    theorem Polynomial.prime_X {R : Type u} [CommRing R] [IsDomain R] :
    Prime Polynomial.X
    theorem Polynomial.irreducible_X_sub_C {R : Type u} [CommRing R] [IsDomain R] (r : R) :
    Irreducible (Polynomial.X - Polynomial.C r)
    theorem Polynomial.irreducible_X {R : Type u} [CommRing R] [IsDomain R] :
    Irreducible Polynomial.X
    theorem Polynomial.eq_of_monic_of_associated {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {q : Polynomial R} (hp : Polynomial.Monic p) (hq : Polynomial.Monic q) (hpq : Associated p q) :
    p = q
    theorem Polynomial.rootMultiplicity_X_sub_C_self {R : Type u} [CommRing R] [IsDomain R] {x : R} :
    Polynomial.rootMultiplicity x (Polynomial.X - Polynomial.C x) = 1
    theorem Polynomial.rootMultiplicity_X_sub_C {R : Type u} [CommRing R] [IsDomain R] [DecidableEq R] {x : R} {y : R} :
    Polynomial.rootMultiplicity x (Polynomial.X - Polynomial.C y) = if x = y then 1 else 0
    theorem Polynomial.rootMultiplicity_X_sub_C_pow {R : Type u} [CommRing R] [IsDomain R] (a : R) (n : ) :
    Polynomial.rootMultiplicity a ((Polynomial.X - Polynomial.C a) ^ n) = n

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

    theorem Polynomial.exists_multiset_roots {R : Type u} [CommRing R] [IsDomain R] [DecidableEq R] {p : Polynomial R} :
    p 0s, ↑(Multiset.card s) Polynomial.degree p ∀ (a : R), Multiset.count a s = Polynomial.rootMultiplicity a p
    noncomputable def Polynomial.roots {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) :

    roots p noncomputably gives a multiset containing all the roots of p, including their multiplicities.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem Polynomial.roots_def {R : Type u} [CommRing R] [IsDomain R] [DecidableEq R] (p : Polynomial R) [Decidable (p = 0)] :
      Polynomial.roots p = if h : p = 0 then else Classical.choose (_ : s, ↑(Multiset.card s) Polynomial.degree p ∀ (a : R), Multiset.count a s = Polynomial.rootMultiplicity a p)
      theorem Polynomial.card_roots {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hp0 : p 0) :
      ↑(Multiset.card (Polynomial.roots p)) Polynomial.degree p
      theorem Polynomial.card_roots_sub_C {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {a : R} (hp0 : 0 < Polynomial.degree p) :
      ↑(Multiset.card (Polynomial.roots (p - Polynomial.C a))) Polynomial.degree p
      theorem Polynomial.card_roots_sub_C' {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {a : R} (hp0 : 0 < Polynomial.degree p) :
      Multiset.card (Polynomial.roots (p - Polynomial.C a)) Polynomial.natDegree p
      @[simp]
      theorem Polynomial.mem_roots {R : Type u} {a : R} [CommRing R] [IsDomain R] {p : Polynomial R} (hp : p 0) :
      theorem Polynomial.ne_zero_of_mem_roots {R : Type u} {a : R} [CommRing R] [IsDomain R] {p : Polynomial R} (h : a Polynomial.roots p) :
      p 0
      theorem Polynomial.exists_max_root {R : Type u} [CommRing R] [IsDomain R] [LinearOrder R] (p : Polynomial R) (hp : p 0) :
      x₀, ∀ (x : R), Polynomial.IsRoot p xx x₀
      theorem Polynomial.exists_min_root {R : Type u} [CommRing R] [IsDomain R] [LinearOrder R] (p : Polynomial R) (hp : p 0) :
      x₀, ∀ (x : R), Polynomial.IsRoot p xx₀ x
      theorem Polynomial.mem_roots_sub_C' {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {a : R} {x : R} :
      x Polynomial.roots (p - Polynomial.C a) p Polynomial.C a Polynomial.eval x p = a
      theorem Polynomial.mem_roots_sub_C {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {a : R} {x : R} (hp0 : 0 < Polynomial.degree p) :
      x Polynomial.roots (p - Polynomial.C a) Polynomial.eval x p = a
      @[simp]
      theorem Polynomial.roots_X_sub_C {R : Type u} [CommRing R] [IsDomain R] (r : R) :
      Polynomial.roots (Polynomial.X - Polynomial.C r) = {r}
      @[simp]
      theorem Polynomial.roots_X {R : Type u} [CommRing R] [IsDomain R] :
      Polynomial.roots Polynomial.X = {0}
      @[simp]
      theorem Polynomial.roots_C {R : Type u} [CommRing R] [IsDomain R] (x : R) :
      Polynomial.roots (Polynomial.C x) = 0
      @[simp]
      theorem Polynomial.roots_C_mul {R : Type u} {a : R} [CommRing R] [IsDomain R] (p : Polynomial R) (ha : a 0) :
      Polynomial.roots (Polynomial.C a * p) = Polynomial.roots p
      @[simp]
      theorem Polynomial.roots_smul_nonzero {R : Type u} {a : R} [CommRing R] [IsDomain R] (p : Polynomial R) (ha : a 0) :
      theorem Polynomial.roots_list_prod {R : Type u} [CommRing R] [IsDomain R] (L : List (Polynomial R)) :
      ¬0 LPolynomial.roots (List.prod L) = Multiset.bind (L) Polynomial.roots
      theorem Polynomial.roots_prod {R : Type u} [CommRing R] [IsDomain R] {ι : Type u_1} (f : ιPolynomial R) (s : Finset ι) :
      @[simp]
      theorem Polynomial.roots_X_pow {R : Type u} [CommRing R] [IsDomain R] (n : ) :
      Polynomial.roots (Polynomial.X ^ n) = n {0}
      theorem Polynomial.roots_C_mul_X_pow {R : Type u} {a : R} [CommRing R] [IsDomain R] (ha : a 0) (n : ) :
      Polynomial.roots (Polynomial.C a * Polynomial.X ^ n) = n {0}
      @[simp]
      theorem Polynomial.roots_monomial {R : Type u} {a : R} [CommRing R] [IsDomain R] (ha : a 0) (n : ) :
      theorem Polynomial.roots_prod_X_sub_C {R : Type u} [CommRing R] [IsDomain R] (s : Finset R) :
      Polynomial.roots (Finset.prod s fun a => Polynomial.X - Polynomial.C a) = s.val
      @[simp]
      theorem Polynomial.roots_multiset_prod_X_sub_C {R : Type u} [CommRing R] [IsDomain R] (s : Multiset R) :
      Polynomial.roots (Multiset.prod (Multiset.map (fun a => Polynomial.X - Polynomial.C a) s)) = s
      @[simp]
      theorem Polynomial.natDegree_multiset_prod_X_sub_C_eq_card {R : Type u} [CommRing R] [IsDomain R] (s : Multiset R) :
      Polynomial.natDegree (Multiset.prod (Multiset.map (fun a => Polynomial.X - Polynomial.C a) s)) = Multiset.card s
      theorem Polynomial.card_roots_X_pow_sub_C {R : Type u} [CommRing R] [IsDomain R] {n : } (hn : 0 < n) (a : R) :
      Multiset.card (Polynomial.roots (Polynomial.X ^ n - Polynomial.C a)) n
      def Polynomial.nthRoots {R : Type u} [CommRing R] [IsDomain R] (n : ) (a : R) :

      nthRoots n a noncomputably returns the solutions to x ^ n = a

      Equations
      Instances For
        @[simp]
        theorem Polynomial.mem_nthRoots {R : Type u} [CommRing R] [IsDomain R] {n : } (hn : 0 < n) {a : R} {x : R} :
        @[simp]
        theorem Polynomial.nthRoots_zero {R : Type u} [CommRing R] [IsDomain R] (r : R) :
        theorem Polynomial.card_nthRoots {R : Type u} [CommRing R] [IsDomain R] (n : ) (a : R) :
        Multiset.card (Polynomial.nthRoots n a) n
        def Polynomial.nthRootsFinset (n : ) (R : Type u_1) [CommRing R] [IsDomain R] :

        The multiset nthRoots ↑n (1 : R) as a Finset.

        Equations
        Instances For
          @[simp]
          theorem Polynomial.mem_nthRootsFinset {R : Type u} [CommRing R] [IsDomain R] {n : } (h : 0 < n) {x : R} :
          theorem Polynomial.Monic.comp_X_add_C {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hp : Polynomial.Monic p) (r : R) :
          Polynomial.Monic (Polynomial.comp p (Polynomial.X + Polynomial.C r))
          theorem Polynomial.Monic.comp_X_sub_C {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hp : Polynomial.Monic p) (r : R) :
          Polynomial.Monic (Polynomial.comp p (Polynomial.X - Polynomial.C r))
          theorem Polynomial.units_coeff_zero_smul {R : Type u} [CommRing R] [IsDomain R] (c : (Polynomial R)ˣ) (p : Polynomial R) :
          Polynomial.coeff (c) 0 p = c * p
          theorem Polynomial.comp_eq_zero_iff {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {q : Polynomial R} :
          Polynomial.comp p q = 0 p = 0 Polynomial.eval (Polynomial.coeff q 0) p = 0 q = Polynomial.C (Polynomial.coeff q 0)
          theorem Polynomial.zero_of_eval_zero {R : Type u} [CommRing R] [IsDomain R] [Infinite R] (p : Polynomial R) (h : ∀ (x : R), Polynomial.eval x p = 0) :
          p = 0
          theorem Polynomial.funext {R : Type u} [CommRing R] [IsDomain R] [Infinite R] {p : Polynomial R} {q : Polynomial R} (ext : ∀ (r : R), Polynomial.eval r p = Polynomial.eval r q) :
          p = q
          @[inline, reducible]
          noncomputable abbrev Polynomial.aroots {T : Type w} [CommRing T] (p : Polynomial T) (S : Type u_1) [CommRing S] [IsDomain S] [Algebra T S] :

          Given a polynomial p with coefficients in a ring T and a T-algebra S, aroots p S is the multiset of roots of p regarded as a polynomial over S.

          Equations
          Instances For
            theorem Polynomial.mem_aroots' {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] {p : Polynomial T} {a : S} :
            theorem Polynomial.mem_aroots {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] [NoZeroSMulDivisors T S] {p : Polynomial T} {a : S} :
            theorem Polynomial.aroots_mul {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] [NoZeroSMulDivisors T S] {p : Polynomial T} {q : Polynomial T} (hpq : p * q 0) :
            @[simp]
            theorem Polynomial.aroots_X_sub_C {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] (r : T) :
            Polynomial.aroots (Polynomial.X - Polynomial.C r) S = {↑(algebraMap T S) r}
            @[simp]
            theorem Polynomial.aroots_X {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] :
            Polynomial.aroots Polynomial.X S = {0}
            @[simp]
            theorem Polynomial.aroots_C {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] (a : T) :
            Polynomial.aroots (Polynomial.C a) S = 0
            @[simp]
            theorem Polynomial.aroots_zero {T : Type w} [CommRing T] (S : Type u_1) [CommRing S] [IsDomain S] [Algebra T S] :
            @[simp]
            theorem Polynomial.aroots_one {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] :
            @[simp]
            theorem Polynomial.aroots_C_mul {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] [NoZeroSMulDivisors T S] {a : T} (p : Polynomial T) (ha : a 0) :
            Polynomial.aroots (Polynomial.C a * p) S = Polynomial.aroots p S
            @[simp]
            theorem Polynomial.aroots_smul_nonzero {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] [NoZeroSMulDivisors T S] {a : T} (p : Polynomial T) (ha : a 0) :
            @[simp]
            theorem Polynomial.aroots_pow {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] (p : Polynomial T) (n : ) :
            theorem Polynomial.aroots_X_pow {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] (n : ) :
            Polynomial.aroots (Polynomial.X ^ n) S = n {0}
            theorem Polynomial.aroots_C_mul_X_pow {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] [NoZeroSMulDivisors T S] {a : T} (ha : a 0) (n : ) :
            Polynomial.aroots (Polynomial.C a * Polynomial.X ^ n) S = n {0}
            @[simp]
            theorem Polynomial.aroots_monomial {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] [NoZeroSMulDivisors T S] {a : T} (ha : a 0) (n : ) :
            def Polynomial.rootSet {T : Type w} [CommRing T] (p : Polynomial T) (S : Type u_1) [CommRing S] [IsDomain S] [Algebra T S] :
            Set S

            The set of distinct roots of p in S.

            If you have a non-separable polynomial, use Polynomial.aroots for the multiset where multiple roots have the appropriate multiplicity.

            Equations
            Instances For
              @[simp]
              theorem Polynomial.rootSet_C {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] (a : T) :
              Polynomial.rootSet (Polynomial.C a) S =
              @[simp]
              theorem Polynomial.rootSet_zero {T : Type w} [CommRing T] (S : Type u_1) [CommRing S] [IsDomain S] [Algebra T S] :
              theorem Polynomial.bUnion_roots_finite {R : Type u_1} {S : Type u_2} [Semiring R] [CommRing S] [IsDomain S] [DecidableEq S] (m : R →+* S) (d : ) {U : Set R} (h : Set.Finite U) :

              The set of roots of all polynomials of bounded degree and having coefficients in a finite set is finite.

              theorem Polynomial.mem_rootSet' {T : Type w} [CommRing T] {p : Polynomial T} {S : Type u_1} [CommRing S] [IsDomain S] [Algebra T S] {a : S} :
              theorem Polynomial.mem_rootSet {T : Type w} [CommRing T] {p : Polynomial T} {S : Type u_1} [CommRing S] [IsDomain S] [Algebra T S] [NoZeroSMulDivisors T S] {a : S} :
              theorem Polynomial.mem_rootSet_of_ne {T : Type w} [CommRing T] {p : Polynomial T} {S : Type u_1} [CommRing S] [IsDomain S] [Algebra T S] [NoZeroSMulDivisors T S] (hp : p 0) {a : S} :
              theorem Polynomial.rootSet_maps_to' {T : Type w} [CommRing T] {p : Polynomial T} {S : Type u_1} {S' : Type u_2} [CommRing S] [IsDomain S] [Algebra T S] [CommRing S'] [IsDomain S'] [Algebra T S'] (hp : Polynomial.map (algebraMap T S') p = 0Polynomial.map (algebraMap T S) p = 0) (f : S →ₐ[T] S') :
              theorem Polynomial.ne_zero_of_mem_rootSet {S : Type v} {T : Type w} [CommRing T] {p : Polynomial T} [CommRing S] [IsDomain S] [Algebra T S] {a : S} (h : a Polynomial.rootSet p S) :
              p 0
              theorem Polynomial.aeval_eq_zero_of_mem_rootSet {S : Type v} {T : Type w} [CommRing T] {p : Polynomial T} [CommRing S] [IsDomain S] [Algebra T S] {a : S} (hx : a Polynomial.rootSet p S) :
              ↑(Polynomial.aeval a) p = 0
              theorem Polynomial.rootSet_mapsTo {T : Type w} [CommRing T] {p : Polynomial T} {S : Type u_1} {S' : Type u_2} [CommRing S] [IsDomain S] [Algebra T S] [CommRing S'] [IsDomain S'] [Algebra T S'] [NoZeroSMulDivisors T S'] (f : S →ₐ[T] S') :

              Division by a monic polynomial doesn't change the leading coefficient.

              theorem Polynomial.leadingCoeff_divByMonic_X_sub_C {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) (hp : Polynomial.degree p 0) (a : R) :
              Polynomial.leadingCoeff (p /ₘ (Polynomial.X - Polynomial.C a)) = Polynomial.leadingCoeff p
              theorem Polynomial.isCoprime_X_sub_C_of_isUnit_sub {R : Type u_1} [CommRing R] {a : R} {b : R} (h : IsUnit (a - b)) :
              IsCoprime (Polynomial.X - Polynomial.C a) (Polynomial.X - Polynomial.C b)
              theorem Polynomial.pairwise_coprime_X_sub_C {K : Type u_1} [Field K] {I : Type v} {s : IK} (H : Function.Injective s) :
              Pairwise (IsCoprime on fun i => Polynomial.X - Polynomial.C (s i))
              theorem Polynomial.monic_prod_multiset_X_sub_C {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} :
              Polynomial.Monic (Multiset.prod (Multiset.map (fun a => Polynomial.X - Polynomial.C a) (Polynomial.roots p)))
              theorem Polynomial.prod_multiset_root_eq_finset_root {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} [DecidableEq R] :
              Multiset.prod (Multiset.map (fun a => Polynomial.X - Polynomial.C a) (Polynomial.roots p)) = Finset.prod (Multiset.toFinset (Polynomial.roots p)) fun a => (Polynomial.X - Polynomial.C a) ^ Polynomial.rootMultiplicity a p
              theorem Polynomial.prod_multiset_X_sub_C_dvd {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) :
              Multiset.prod (Multiset.map (fun a => Polynomial.X - Polynomial.C a) (Polynomial.roots p)) p

              The product ∏ (X - a) for a inside the multiset p.roots divides p.

              theorem Multiset.prod_X_sub_C_dvd_iff_le_roots {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hp : p 0) (s : Multiset R) :
              Multiset.prod (Multiset.map (fun a => Polynomial.X - Polynomial.C a) s) p s Polynomial.roots p

              A Galois connection.

              theorem Polynomial.exists_prod_multiset_X_sub_C_mul {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) :
              q, Multiset.prod (Multiset.map (fun a => Polynomial.X - Polynomial.C a) (Polynomial.roots p)) * q = p Multiset.card (Polynomial.roots p) + Polynomial.natDegree q = Polynomial.natDegree p Polynomial.roots q = 0
              theorem Polynomial.C_leadingCoeff_mul_prod_multiset_X_sub_C {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hroots : Multiset.card (Polynomial.roots p) = Polynomial.natDegree p) :
              Polynomial.C (Polynomial.leadingCoeff p) * Multiset.prod (Multiset.map (fun a => Polynomial.X - Polynomial.C a) (Polynomial.roots p)) = p

              A polynomial p that has as many roots as its degree can be written p = p.leadingCoeff * ∏(X - a), for a in p.roots.

              theorem Polynomial.prod_multiset_X_sub_C_of_monic_of_roots_card_eq {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hp : Polynomial.Monic p) (hroots : Multiset.card (Polynomial.roots p) = Polynomial.natDegree p) :
              Multiset.prod (Multiset.map (fun a => Polynomial.X - Polynomial.C a) (Polynomial.roots p)) = p

              A monic polynomial p that has as many roots as its degree can be written p = ∏(X - a), for a in p.roots.

              theorem Polynomial.card_roots_le_map {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] {p : Polynomial A} {f : A →+* B} (h : Polynomial.map f p 0) :
              Multiset.card (Polynomial.roots p) Multiset.card (Polynomial.roots (Polynomial.map f p))
              theorem Polynomial.card_roots_le_map_of_injective {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] {p : Polynomial A} {f : A →+* B} (hf : Function.Injective f) :
              Multiset.card (Polynomial.roots p) Multiset.card (Polynomial.roots (Polynomial.map f p))
              theorem Polynomial.Monic.irreducible_of_irreducible_map {R : Type u} {S : Type v} [CommRing R] [IsDomain R] [CommRing S] [IsDomain S] (φ : R →+* S) (f : Polynomial R) (h_mon : Polynomial.Monic f) (h_irr : Irreducible (Polynomial.map φ f)) :

              A polynomial over an integral domain R is irreducible if it is monic and irreducible after mapping into an integral domain S.

              A special case of this lemma is that a polynomial over is irreducible if it is monic and irreducible over ℤ/pℤ for some prime p.