Documentation

Mathlib.Algebra.Polynomial.Roots

Theory of univariate polynomials #

We define the multiset of roots of a polynomial, and prove basic results about it.

Main definitions #

Main statements #

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
Instances For
    theorem Polynomial.roots_def {R : Type u} [CommRing R] [IsDomain R] [DecidableEq R] (p : Polynomial R) [Decidable (p = 0)] :
    p.roots = if h : p = 0 then else Classical.choose
    theorem Polynomial.card_roots {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hp0 : p 0) :
    (Multiset.card p.roots) p.degree
    theorem Polynomial.card_roots' {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) :
    Multiset.card p.roots p.natDegree
    theorem Polynomial.card_roots_sub_C {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {a : R} (hp0 : 0 < p.degree) :
    (Multiset.card (p - Polynomial.C a).roots) p.degree
    theorem Polynomial.card_roots_sub_C' {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {a : R} (hp0 : 0 < p.degree) :
    Multiset.card (p - Polynomial.C a).roots p.natDegree
    @[simp]
    @[simp]
    theorem Polynomial.mem_roots' {R : Type u} {a : R} [CommRing R] [IsDomain R] {p : Polynomial R} :
    a p.roots p 0 p.IsRoot a
    theorem Polynomial.mem_roots {R : Type u} {a : R} [CommRing R] [IsDomain R] {p : Polynomial R} (hp : p 0) :
    a p.roots p.IsRoot a
    theorem Polynomial.ne_zero_of_mem_roots {R : Type u} {a : R} [CommRing R] [IsDomain R] {p : Polynomial R} (h : a p.roots) :
    p 0
    theorem Polynomial.isRoot_of_mem_roots {R : Type u} {a : R} [CommRing R] [IsDomain R] {p : Polynomial R} (h : a p.roots) :
    p.IsRoot a
    theorem Polynomial.mem_roots_map_of_injective {R : Type u} {S : Type v} [CommRing R] [IsDomain R] [Semiring S] {p : Polynomial S} {f : S →+* R} (hf : Function.Injective f) {x : R} (hp : p 0) :
    x (Polynomial.map f p).roots Polynomial.eval₂ f x p = 0
    theorem Polynomial.mem_roots_iff_aeval_eq_zero {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {x : R} (w : p 0) :
    x p.roots (Polynomial.aeval x) p = 0
    theorem Polynomial.card_le_degree_of_subset_roots {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {Z : Finset R} (h : Z.val p.roots) :
    Z.card p.natDegree
    theorem Polynomial.finite_setOf_isRoot {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hp : p 0) :
    {x : R | p.IsRoot x}.Finite
    theorem Polynomial.eq_zero_of_infinite_isRoot {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) (h : {x : R | p.IsRoot x}.Infinite) :
    p = 0
    theorem Polynomial.exists_max_root {R : Type u} [CommRing R] [IsDomain R] [LinearOrder R] (p : Polynomial R) (hp : p 0) :
    ∃ (x₀ : R), ∀ (x : R), p.IsRoot xx x₀
    theorem Polynomial.exists_min_root {R : Type u} [CommRing R] [IsDomain R] [LinearOrder R] (p : Polynomial R) (hp : p 0) :
    ∃ (x₀ : R), ∀ (x : R), p.IsRoot xx₀ x
    theorem Polynomial.eq_of_infinite_eval_eq {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) (q : Polynomial R) (h : {x : R | Polynomial.eval x p = Polynomial.eval x q}.Infinite) :
    p = q
    theorem Polynomial.roots_mul {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {q : Polynomial R} (hpq : p * q 0) :
    (p * q).roots = p.roots + q.roots
    theorem Polynomial.roots.le_of_dvd {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {q : Polynomial R} (h : q 0) :
    p qp.roots q.roots
    theorem Polynomial.mem_roots_sub_C' {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {a : R} {x : R} :
    x (p - Polynomial.C a).roots 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 < p.degree) :
    x (p - Polynomial.C a).roots Polynomial.eval x p = a
    @[simp]
    theorem Polynomial.roots_X_sub_C {R : Type u} [CommRing R] [IsDomain R] (r : R) :
    (Polynomial.X - Polynomial.C r).roots = {r}
    @[simp]
    theorem Polynomial.roots_X {R : Type u} [CommRing R] [IsDomain R] :
    Polynomial.X.roots = {0}
    @[simp]
    theorem Polynomial.roots_C {R : Type u} [CommRing R] [IsDomain R] (x : R) :
    (Polynomial.C x).roots = 0
    @[simp]
    theorem Polynomial.roots_C_mul {R : Type u} {a : R} [CommRing R] [IsDomain R] (p : Polynomial R) (ha : a 0) :
    (Polynomial.C a * p).roots = p.roots
    @[simp]
    theorem Polynomial.roots_smul_nonzero {R : Type u} {a : R} [CommRing R] [IsDomain R] (p : Polynomial R) (ha : a 0) :
    (a p).roots = p.roots
    @[simp]
    theorem Polynomial.roots_neg {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) :
    (-p).roots = p.roots
    theorem Polynomial.roots_list_prod {R : Type u} [CommRing R] [IsDomain R] (L : List (Polynomial R)) :
    0LL.prod.roots = (↑L).bind Polynomial.roots
    theorem Polynomial.roots_multiset_prod {R : Type u} [CommRing R] [IsDomain R] (m : Multiset (Polynomial R)) :
    0mm.prod.roots = m.bind Polynomial.roots
    theorem Polynomial.roots_prod {R : Type u} [CommRing R] [IsDomain R] {ι : Type u_1} (f : ιPolynomial R) (s : Finset ι) :
    s.prod f 0(s.prod f).roots = s.val.bind fun (i : ι) => (f i).roots
    @[simp]
    theorem Polynomial.roots_pow {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) (n : ) :
    (p ^ n).roots = n p.roots
    theorem Polynomial.roots_X_pow {R : Type u} [CommRing R] [IsDomain R] (n : ) :
    (Polynomial.X ^ n).roots = n {0}
    theorem Polynomial.roots_C_mul_X_pow {R : Type u} {a : R} [CommRing R] [IsDomain R] (ha : a 0) (n : ) :
    (Polynomial.C a * Polynomial.X ^ n).roots = n {0}
    @[simp]
    theorem Polynomial.roots_monomial {R : Type u} {a : R} [CommRing R] [IsDomain R] (ha : a 0) (n : ) :
    ((Polynomial.monomial n) a).roots = n {0}
    theorem Polynomial.roots_prod_X_sub_C {R : Type u} [CommRing R] [IsDomain R] (s : Finset R) :
    (∏ as, (Polynomial.X - Polynomial.C a)).roots = s.val
    @[simp]
    theorem Polynomial.roots_multiset_prod_X_sub_C {R : Type u} [CommRing R] [IsDomain R] (s : Multiset R) :
    (Multiset.map (fun (a : R) => Polynomial.X - Polynomial.C a) s).prod.roots = 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.X ^ n - Polynomial.C a).roots 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.mul_mem_nthRootsFinset {R : Type u} {n : } [CommRing R] [IsDomain R] {η₁ : R} {η₂ : R} (hη₁ : η₁ Polynomial.nthRootsFinset n R) (hη₂ : η₂ Polynomial.nthRootsFinset n R) :
        theorem Polynomial.ne_zero_of_mem_nthRootsFinset {R : Type u} {n : } [CommRing R] [IsDomain R] {η : R} (hη : η Polynomial.nthRootsFinset n R) :
        η 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
        @[reducible, inline]
        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.aroots_def {T : Type w} [CommRing T] (p : Polynomial T) (S : Type u_1) [CommRing S] [IsDomain S] [Algebra T S] :
          p.aroots S = (Polynomial.map (algebraMap T S) p).roots
          theorem Polynomial.mem_aroots' {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] {p : Polynomial T} {a : S} :
          a p.aroots S Polynomial.map (algebraMap T S) p 0 (Polynomial.aeval a) p = 0
          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} :
          a p.aroots S p 0 (Polynomial.aeval a) p = 0
          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) :
          (p * q).aroots S = p.aroots S + q.aroots S
          @[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.X - Polynomial.C r).aroots 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.X.aroots 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.C a).aroots 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_neg {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] (p : Polynomial T) :
          (-p).aroots S = p.aroots 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.C a * p).aroots S = p.aroots 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) :
          (a p).aroots S = p.aroots S
          @[simp]
          theorem Polynomial.aroots_pow {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] (p : Polynomial T) (n : ) :
          (p ^ n).aroots S = n p.aroots S
          theorem Polynomial.aroots_X_pow {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] (n : ) :
          (Polynomial.X ^ n).aroots 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.C a * Polynomial.X ^ n).aroots 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 : ) :
          ((Polynomial.monomial n) a).aroots S = n {0}
          @[simp]
          theorem Polynomial.aroots_map (R : Type u) (S : Type v) {T : Type w} [CommRing R] [IsDomain R] [CommRing T] (p : Polynomial T) [CommRing S] [Algebra T S] [Algebra S R] [Algebra T R] [IsScalarTower T S R] :
          (Polynomial.map (algebraMap T S) p).aroots R = p.aroots R
          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
          • p.rootSet S = (p.aroots S).toFinset
          Instances For
            theorem Polynomial.rootSet_def {T : Type w} [CommRing T] (p : Polynomial T) (S : Type u_1) [CommRing S] [IsDomain S] [Algebra T S] [DecidableEq S] :
            p.rootSet S = (p.aroots S).toFinset
            @[simp]
            theorem Polynomial.rootSet_C {S : Type v} {T : Type w} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] (a : T) :
            (Polynomial.C a).rootSet S =
            @[simp]
            theorem Polynomial.rootSet_zero {T : Type w} [CommRing T] (S : Type u_1) [CommRing S] [IsDomain S] [Algebra T S] :
            @[simp]
            theorem Polynomial.rootSet_one {T : Type w} [CommRing T] (S : Type u_1) [CommRing S] [IsDomain S] [Algebra T S] :
            @[simp]
            theorem Polynomial.rootSet_neg {T : Type w} [CommRing T] (p : Polynomial T) (S : Type u_1) [CommRing S] [IsDomain S] [Algebra T S] :
            (-p).rootSet S = p.rootSet S
            instance Polynomial.rootSetFintype {T : Type w} [CommRing T] (p : Polynomial T) (S : Type u_1) [CommRing S] [IsDomain S] [Algebra T S] :
            Fintype (p.rootSet S)
            Equations
            theorem Polynomial.rootSet_finite {T : Type w} [CommRing T] (p : Polynomial T) (S : Type u_1) [CommRing S] [IsDomain S] [Algebra T S] :
            (p.rootSet S).Finite
            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 : U.Finite) :
            (⋃ (f : Polynomial R), ⋃ (_ : f.natDegree d ∀ (i : ), f.coeff i U), (Polynomial.map m f).roots.toFinset).Finite

            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} :
            a p.rootSet S Polynomial.map (algebraMap T S) p 0 (Polynomial.aeval a) p = 0
            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} :
            a p.rootSet S p 0 (Polynomial.aeval a) p = 0
            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} :
            a p.rootSet S (Polynomial.aeval a) p = 0
            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') :
            Set.MapsTo (⇑f) (p.rootSet S) (p.rootSet 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 p.rootSet 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 p.rootSet S) :
            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') :
            Set.MapsTo (⇑f) (p.rootSet S) (p.rootSet S')
            theorem Polynomial.mem_rootSet_of_injective {R : Type u} {S : Type v} [CommRing R] [IsDomain R] [CommRing S] {p : Polynomial S} [Algebra S R] (h : Function.Injective (algebraMap S R)) {x : R} (hp : p 0) :
            x p.rootSet R (Polynomial.aeval x) p = 0
            theorem Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero {R : Type u_1} [CommRing R] [IsDomain R] (p : Polynomial R) {ι : Type u_2} [Fintype ι] {f : ιR} (hf : Function.Injective f) (heval : ∀ (i : ι), Polynomial.eval (f i) p = 0) (hcard : p.natDegree < Fintype.card ι) :
            p = 0
            theorem Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero' {R : Type u_1} [CommRing R] [IsDomain R] (p : Polynomial R) (s : Finset R) (heval : is, Polynomial.eval i p = 0) (hcard : p.natDegree < s.card) :
            p = 0
            theorem Polynomial.eq_zero_of_forall_eval_zero_of_natDegree_lt_card {R : Type u} [CommRing R] [IsDomain R] (f : Polynomial R) (hf : ∀ (r : R), Polynomial.eval r f = 0) (hfR : f.natDegree < Cardinal.mk R) :
            f = 0
            theorem Polynomial.exists_eval_ne_zero_of_natDegree_lt_card {R : Type u} [CommRing R] [IsDomain R] (f : Polynomial R) (hf : f 0) (hfR : f.natDegree < Cardinal.mk R) :
            ∃ (r : R), Polynomial.eval r f 0
            theorem Polynomial.monic_prod_multiset_X_sub_C {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} :
            (Multiset.map (fun (a : R) => Polynomial.X - Polynomial.C a) p.roots).prod.Monic
            theorem Polynomial.prod_multiset_root_eq_finset_root {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} [DecidableEq R] :
            (Multiset.map (fun (a : R) => Polynomial.X - Polynomial.C a) p.roots).prod = ap.roots.toFinset, (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.map (fun (a : R) => Polynomial.X - Polynomial.C a) p.roots).prod 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.map (fun (a : R) => Polynomial.X - Polynomial.C a) s).prod p s p.roots

            A Galois connection.

            theorem Polynomial.exists_prod_multiset_X_sub_C_mul {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) :
            ∃ (q : Polynomial R), (Multiset.map (fun (a : R) => Polynomial.X - Polynomial.C a) p.roots).prod * q = p Multiset.card p.roots + q.natDegree = p.natDegree q.roots = 0
            theorem Polynomial.C_leadingCoeff_mul_prod_multiset_X_sub_C {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hroots : Multiset.card p.roots = p.natDegree) :
            Polynomial.C p.leadingCoeff * (Multiset.map (fun (a : R) => Polynomial.X - Polynomial.C a) p.roots).prod = 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 : p.Monic) (hroots : Multiset.card p.roots = p.natDegree) :
            (Multiset.map (fun (a : R) => Polynomial.X - Polynomial.C a) p.roots).prod = 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.Monic.isUnit_leadingCoeff_of_dvd {R : Type u} [CommRing R] [IsDomain R] {a : Polynomial R} {p : Polynomial R} (hp : p.Monic) (hap : a p) :
            IsUnit a.leadingCoeff
            theorem Polynomial.Monic.irreducible_iff_degree_lt {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (p_monic : p.Monic) (p_1 : p 1) :
            Irreducible p ∀ (q : Polynomial R), q.degree (p.natDegree / 2)q pIsUnit q

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

            See also: Polynomial.Monic.irreducible_iff_natDegree.

            theorem Polynomial.count_map_roots {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDomain A] [DecidableEq B] {p : Polynomial A} {f : A →+* B} (hmap : Polynomial.map f p 0) (b : B) :
            theorem Polynomial.map_roots_le {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.map (⇑f) p.roots (Polynomial.map f p).roots
            theorem Polynomial.map_roots_le_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.map (⇑f) p.roots (Polynomial.map f 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 p.roots Multiset.card (Polynomial.map f p).roots
            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 p.roots Multiset.card (Polynomial.map f p).roots
            theorem Polynomial.roots_map_of_injective_of_card_eq_natDegree {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) (hroots : Multiset.card p.roots = p.natDegree) :
            Multiset.map (⇑f) p.roots = (Polynomial.map f p).roots