Documentation

Mathlib.RingTheory.Polynomial.Basic

Ring-theoretic supplement of Algebra.Polynomial. #

Main results #

instance Polynomial.instCharP {R : Type u} [Semiring R] (p : ) [h : CharP R p] :
Equations
  • =
instance Polynomial.instExpChar {R : Type u} [Semiring R] (p : ) [h : ExpChar R p] :
Equations
  • =

The R-submodule of R[X] consisting of polynomials of degree ≤ n.

Equations
Instances For

    The R-submodule of R[X] consisting of polynomials of degree < n.

    Equations
    Instances For
      theorem Polynomial.mem_degreeLE {R : Type u} [Semiring R] {n : WithBot } {f : Polynomial R} :
      f Polynomial.degreeLE R n f.degree n
      theorem Polynomial.degreeLE_eq_span_X_pow {R : Type u} [Semiring R] [DecidableEq R] {n : } :
      Polynomial.degreeLE R n = Submodule.span R (Finset.image (fun (n : ) => Polynomial.X ^ n) (Finset.range (n + 1)))
      theorem Polynomial.mem_degreeLT {R : Type u} [Semiring R] {n : } {f : Polynomial R} :
      f Polynomial.degreeLT R n f.degree < n
      theorem Polynomial.degreeLT_eq_span_X_pow {R : Type u} [Semiring R] [DecidableEq R] {n : } :
      Polynomial.degreeLT R n = Submodule.span R (Finset.image (fun (n : ) => Polynomial.X ^ n) (Finset.range n))
      def Polynomial.degreeLTEquiv (R : Type u_2) [Semiring R] (n : ) :
      (Polynomial.degreeLT R n) ≃ₗ[R] Fin nR

      The first n coefficients on degreeLT n form a linear equivalence with Fin n → R.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem Polynomial.eval_eq_sum_degreeLTEquiv {R : Type u} [Semiring R] {n : } {p : Polynomial R} (hp : p Polynomial.degreeLT R n) (x : R) :
        Polynomial.eval x p = i : Fin n, (Polynomial.degreeLTEquiv R n) p, hp i * x ^ i
        theorem Polynomial.exists_degree_le_of_mem_span {R : Type u} [Semiring R] {s : Set (Polynomial R)} {p : Polynomial R} (hs : s.Nonempty) (hp : p Submodule.span R s) :
        p's, p.degree p'.degree

        For every polynomial p in the span of a set s : Set R[X], there exists a polynomial of p' ∈ s with higher degree. See also Polynomial.exists_degree_le_of_mem_span_of_finite.

        theorem Polynomial.exists_degree_le_of_mem_span_of_finite {R : Type u} [Semiring R] {s : Set (Polynomial R)} (s_fin : s.Finite) (hs : s.Nonempty) :
        p's, pSubmodule.span R s, p.degree p'.degree

        A stronger version of Polynomial.exists_degree_le_of_mem_span under the assumption that the set s : R[X] is finite. There exists a polynomial p' ∈ s whose degree dominates the degree of every element of p ∈ span R s

        theorem Polynomial.span_le_degreeLE_of_finite {R : Type u} [Semiring R] {s : Set (Polynomial R)} (s_fin : s.Finite) :

        The span of every finite set of polynomials is contained in a degreeLE n for some n.

        theorem Polynomial.span_of_finite_le_degreeLT {R : Type u} [Semiring R] {s : Set (Polynomial R)} (s_fin : s.Finite) :

        The span of every finite set of polynomials is contained in a degreeLT n for some n.

        If R is a nontrivial ring, the polynomials R[X] are not finite as an R-module. When R is a field, this is equivalent to R[X] being an infinite-dimensional vector space over R.

        def Polynomial.coeffs {R : Type u} [Semiring R] (p : Polynomial R) :

        The finset of nonzero coefficients of a polynomial.

        Equations
        Instances For
          @[deprecated Polynomial.coeffs]
          def Polynomial.frange {R : Type u} [Semiring R] (p : Polynomial R) :

          Alias of Polynomial.coeffs.


          The finset of nonzero coefficients of a polynomial.

          Equations
          Instances For
            @[deprecated Polynomial.coeffs_zero]

            Alias of Polynomial.coeffs_zero.

            theorem Polynomial.mem_coeffs_iff {R : Type u} [Semiring R] {p : Polynomial R} {c : R} :
            c p.coeffs np.support, c = p.coeff n
            @[deprecated Polynomial.mem_coeffs_iff]
            theorem Polynomial.mem_frange_iff {R : Type u} [Semiring R] {p : Polynomial R} {c : R} :
            c p.coeffs np.support, c = p.coeff n

            Alias of Polynomial.mem_coeffs_iff.

            @[deprecated Polynomial.coeffs_one]

            Alias of Polynomial.coeffs_one.

            theorem Polynomial.coeff_mem_coeffs {R : Type u} [Semiring R] (p : Polynomial R) (n : ) (h : p.coeff n 0) :
            p.coeff n p.coeffs
            @[deprecated Polynomial.coeff_mem_coeffs]
            theorem Polynomial.coeff_mem_frange {R : Type u} [Semiring R] (p : Polynomial R) (n : ) (h : p.coeff n 0) :
            p.coeff n p.coeffs

            Alias of Polynomial.coeff_mem_coeffs.

            theorem Polynomial.geom_sum_X_comp_X_add_one_eq_sum {R : Type u} [Semiring R] (n : ) :
            (iFinset.range n, Polynomial.X ^ i).comp (Polynomial.X + 1) = iFinset.range n, (n.choose (i + 1)) * Polynomial.X ^ i
            theorem Polynomial.Monic.geom_sum {R : Type u} [Semiring R] {P : Polynomial R} (hP : P.Monic) (hdeg : 0 < P.natDegree) {n : } (hn : n 0) :
            (iFinset.range n, P ^ i).Monic
            theorem Polynomial.Monic.geom_sum' {R : Type u} [Semiring R] {P : Polynomial R} (hP : P.Monic) (hdeg : 0 < P.degree) {n : } (hn : n 0) :
            (iFinset.range n, P ^ i).Monic
            theorem Polynomial.monic_geom_sum_X {R : Type u} [Semiring R] {n : } (hn : n 0) :
            (iFinset.range n, Polynomial.X ^ i).Monic
            def Polynomial.restriction {R : Type u} [Ring R] (p : Polynomial R) :
            Polynomial (Subring.closure p.coeffs)

            Given a polynomial, return the polynomial whose coefficients are in the ring closure of the original coefficients.

            Equations
            Instances For
              @[simp]
              theorem Polynomial.coeff_restriction {R : Type u} [Ring R] {p : Polynomial R} {n : } :
              (p.restriction.coeff n) = p.coeff n
              theorem Polynomial.coeff_restriction' {R : Type u} [Ring R] {p : Polynomial R} {n : } :
              (p.restriction.coeff n) = p.coeff n
              @[simp]
              theorem Polynomial.support_restriction {R : Type u} [Ring R] (p : Polynomial R) :
              p.restriction.support = p.support
              @[simp]
              theorem Polynomial.map_restriction {R : Type u} [CommRing R] (p : Polynomial R) :
              Polynomial.map (algebraMap ((Subring.closure p.coeffs)) R) p.restriction = p
              @[simp]
              theorem Polynomial.degree_restriction {R : Type u} [Ring R] {p : Polynomial R} :
              p.restriction.degree = p.degree
              @[simp]
              theorem Polynomial.natDegree_restriction {R : Type u} [Ring R] {p : Polynomial R} :
              p.restriction.natDegree = p.natDegree
              @[simp]
              theorem Polynomial.monic_restriction {R : Type u} [Ring R] {p : Polynomial R} :
              p.restriction.Monic p.Monic
              theorem Polynomial.eval₂_restriction {R : Type u} {S : Type u_1} [Ring R] [Semiring S] {f : R →+* S} {x : S} {p : Polynomial R} :
              Polynomial.eval₂ f x p = Polynomial.eval₂ (f.comp (Subring.closure p.coeffs).subtype) x p.restriction
              def Polynomial.toSubring {R : Type u} [Ring R] (p : Polynomial R) (T : Subring R) (hp : p.coeffs T) :

              Given a polynomial p and a subring T that contains the coefficients of p, return the corresponding polynomial whose coefficients are in T.

              Equations
              Instances For
                @[simp]
                theorem Polynomial.coeff_toSubring {R : Type u} [Ring R] (p : Polynomial R) (T : Subring R) (hp : p.coeffs T) {n : } :
                ((p.toSubring T hp).coeff n) = p.coeff n
                theorem Polynomial.coeff_toSubring' {R : Type u} [Ring R] (p : Polynomial R) (T : Subring R) (hp : p.coeffs T) {n : } :
                ((p.toSubring T hp).coeff n) = p.coeff n
                @[simp]
                theorem Polynomial.support_toSubring {R : Type u} [Ring R] (p : Polynomial R) (T : Subring R) (hp : p.coeffs T) :
                (p.toSubring T hp).support = p.support
                @[simp]
                theorem Polynomial.degree_toSubring {R : Type u} [Ring R] (p : Polynomial R) (T : Subring R) (hp : p.coeffs T) :
                (p.toSubring T hp).degree = p.degree
                @[simp]
                theorem Polynomial.natDegree_toSubring {R : Type u} [Ring R] (p : Polynomial R) (T : Subring R) (hp : p.coeffs T) :
                (p.toSubring T hp).natDegree = p.natDegree
                @[simp]
                theorem Polynomial.monic_toSubring {R : Type u} [Ring R] (p : Polynomial R) (T : Subring R) (hp : p.coeffs T) :
                (p.toSubring T hp).Monic p.Monic
                @[simp]
                theorem Polynomial.toSubring_zero {R : Type u} [Ring R] (T : Subring R) :
                @[simp]
                theorem Polynomial.toSubring_one {R : Type u} [Ring R] (T : Subring R) :
                @[simp]
                theorem Polynomial.map_toSubring {R : Type u} [Ring R] (p : Polynomial R) (T : Subring R) (hp : p.coeffs T) :
                Polynomial.map T.subtype (p.toSubring T hp) = p
                def Polynomial.ofSubring {R : Type u} [Ring R] (T : Subring R) (p : Polynomial T) :

                Given a polynomial whose coefficients are in some subring, return the corresponding polynomial whose coefficients are in the ambient ring.

                Equations
                Instances For
                  theorem Polynomial.coeff_ofSubring {R : Type u} [Ring R] (T : Subring R) (p : Polynomial T) (n : ) :
                  (Polynomial.ofSubring T p).coeff n = (p.coeff n)
                  @[simp]
                  theorem Polynomial.coeffs_ofSubring {R : Type u} [Ring R] (T : Subring R) {p : Polynomial T} :
                  (Polynomial.ofSubring T p).coeffs T
                  @[deprecated Polynomial.coeffs_ofSubring]
                  theorem Polynomial.frange_ofSubring {R : Type u} [Ring R] (T : Subring R) {p : Polynomial T} :
                  (Polynomial.ofSubring T p).coeffs T

                  Alias of Polynomial.coeffs_ofSubring.

                  theorem Polynomial.mem_ker_modByMonic {R : Type u} [CommRing R] {q : Polynomial R} (hq : q.Monic) {p : Polynomial R} :
                  p LinearMap.ker q.modByMonicHom q p
                  @[simp]
                  theorem Polynomial.ker_modByMonicHom {R : Type u} [CommRing R] {q : Polynomial R} (hq : q.Monic) :

                  Transport an ideal of R[X] to an R-submodule of R[X].

                  Equations
                  • I.ofPolynomial = { carrier := I.carrier, add_mem' := , zero_mem' := , smul_mem' := }
                  Instances For
                    theorem Ideal.mem_ofPolynomial {R : Type u} [Semiring R] {I : Ideal (Polynomial R)} (x : Polynomial R) :
                    x I.ofPolynomial x I
                    def Ideal.degreeLE {R : Type u} [Semiring R] (I : Ideal (Polynomial R)) (n : WithBot ) :

                    Given an ideal I of R[X], make the R-submodule of I consisting of polynomials of degree ≤ n.

                    Equations
                    Instances For
                      def Ideal.leadingCoeffNth {R : Type u} [Semiring R] (I : Ideal (Polynomial R)) (n : ) :

                      Given an ideal I of R[X], make the ideal in R of leading coefficients of polynomials in I with degree ≤ n.

                      Equations
                      Instances For
                        def Ideal.leadingCoeff {R : Type u} [Semiring R] (I : Ideal (Polynomial R)) :

                        Given an ideal I in R[X], make the ideal in R of the leading coefficients in I.

                        Equations
                        • I.leadingCoeff = ⨆ (n : ), I.leadingCoeffNth n
                        Instances For
                          theorem Ideal.polynomial_mem_ideal_of_coeff_mem_ideal {R : Type u} [CommSemiring R] (I : Ideal (Polynomial R)) (p : Polynomial R) (hp : ∀ (n : ), p.coeff n Ideal.comap Polynomial.C I) :
                          p I

                          If every coefficient of a polynomial is in an ideal I, then so is the polynomial itself

                          theorem Ideal.mem_map_C_iff {R : Type u} [CommSemiring R] {I : Ideal R} {f : Polynomial R} :
                          f Ideal.map Polynomial.C I ∀ (n : ), f.coeff n I

                          The push-forward of an ideal I of R to R[X] via inclusion is exactly the set of polynomials whose coefficients are in I

                          theorem Polynomial.ker_mapRingHom {R : Type u} {S : Type u_1} [CommSemiring R] [Semiring S] (f : R →+* S) :
                          LinearMap.ker (Polynomial.mapRingHom f).toSemilinearMap = Ideal.map Polynomial.C (RingHom.ker f)
                          theorem Ideal.mem_leadingCoeffNth {R : Type u} [CommSemiring R] (I : Ideal (Polynomial R)) (n : ) (x : R) :
                          x I.leadingCoeffNth n pI, p.degree n p.leadingCoeff = x
                          theorem Ideal.mem_leadingCoeffNth_zero {R : Type u} [CommSemiring R] (I : Ideal (Polynomial R)) (x : R) :
                          x I.leadingCoeffNth 0 Polynomial.C x I
                          theorem Ideal.leadingCoeffNth_mono {R : Type u} [CommSemiring R] (I : Ideal (Polynomial R)) {m : } {n : } (H : m n) :
                          I.leadingCoeffNth m I.leadingCoeffNth n
                          theorem Ideal.mem_leadingCoeff {R : Type u} [CommSemiring R] (I : Ideal (Polynomial R)) (x : R) :
                          x I.leadingCoeff pI, p.leadingCoeff = x
                          theorem Polynomial.coeff_prod_mem_ideal_pow_tsub {R : Type u} [CommSemiring R] {ι : Type u_2} (s : Finset ι) (f : ιPolynomial R) (I : Ideal R) (n : ι) (h : is, ∀ (k : ), (f i).coeff k I ^ (n i - k)) (k : ) :
                          (s.prod f).coeff k I ^ (s.sum n - k)

                          If I is an ideal, and pᵢ is a finite family of polynomials each satisfying ∀ k, (pᵢ)ₖ ∈ Iⁿⁱ⁻ᵏ for some nᵢ, then p = ∏ pᵢ also satisfies ∀ k, pₖ ∈ Iⁿ⁻ᵏ with n = ∑ nᵢ.

                          R[X] is never a field for any ring R.

                          theorem Ideal.eq_zero_of_constant_mem_of_maximal {R : Type u} [Ring R] (hR : IsField R) (I : Ideal (Polynomial R)) [hI : I.IsMaximal] (x : R) (hx : Polynomial.C x I) :
                          x = 0

                          The only constant in a maximal ideal over a field is 0.

                          theorem Ideal.isPrime_map_C_iff_isPrime {R : Type u} [CommRing R] (P : Ideal R) :
                          (Ideal.map Polynomial.C P).IsPrime P.IsPrime

                          If P is a prime ideal of R, then P.R[x] is a prime ideal of R[x].

                          theorem Ideal.isPrime_map_C_of_isPrime {R : Type u} [CommRing R] {P : Ideal R} (H : P.IsPrime) :
                          (Ideal.map Polynomial.C P).IsPrime

                          If P is a prime ideal of R, then P.R[x] is a prime ideal of R[x].

                          theorem Ideal.is_fg_degreeLE {R : Type u} [CommRing R] [IsNoetherianRing R] (I : Ideal (Polynomial R)) (n : ) :
                          (I.degreeLE n).FG
                          theorem Polynomial.prime_C_iff {R : Type u} [CommRing R] {r : R} :
                          Prime (Polynomial.C r) Prime r
                          theorem MvPolynomial.prime_C_iff {R : Type u} (σ : Type v) [CommRing R] {r : R} :
                          Prime (MvPolynomial.C r) Prime r
                          theorem MvPolynomial.prime_rename_iff {R : Type u} {σ : Type v} [CommRing R] (s : Set σ) {p : MvPolynomial (s) R} :
                          Prime ((MvPolynomial.rename Subtype.val) p) Prime p
                          @[instance 100]
                          Equations
                          • =

                          Hilbert basis theorem: a polynomial ring over a noetherian ring is a noetherian ring.

                          theorem Polynomial.exists_irreducible_of_degree_pos {R : Type u} [CommRing R] [IsDomain R] [WfDvdMonoid R] {f : Polynomial R} (hf : 0 < f.degree) :
                          ∃ (g : Polynomial R), Irreducible g g f
                          theorem Polynomial.exists_irreducible_of_natDegree_pos {R : Type u} [CommRing R] [IsDomain R] [WfDvdMonoid R] {f : Polynomial R} (hf : 0 < f.natDegree) :
                          ∃ (g : Polynomial R), Irreducible g g f
                          theorem Polynomial.exists_irreducible_of_natDegree_ne_zero {R : Type u} [CommRing R] [IsDomain R] [WfDvdMonoid R] {f : Polynomial R} (hf : f.natDegree 0) :
                          ∃ (g : Polynomial R), Irreducible g g f
                          theorem Polynomial.linearIndependent_powers_iff_aeval {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : M →ₗ[R] M) (v : M) :
                          (LinearIndependent R fun (n : ) => (f ^ n) v) ∀ (p : Polynomial R), ((Polynomial.aeval f) p) v = 0p = 0
                          theorem MvPolynomial.aeval_natDegree_le {σ : Type v} {R : Type u_2} [CommSemiring R] {m : } {n : } (F : MvPolynomial σ R) (hF : F.totalDegree m) (f : σPolynomial R) (hf : ∀ (i : σ), (f i).natDegree n) :
                          ((MvPolynomial.aeval f) F).natDegree m * n

                          The multivariate polynomial ring in finitely many variables over a noetherian ring is itself a noetherian ring.

                          Equations
                          • =

                          Auxiliary lemma: Multivariate polynomials over an integral domain with variables indexed by Fin n form an integral domain. This fact is proven inductively, and then used to prove the general case without any finiteness hypotheses. See MvPolynomial.noZeroDivisors for the general case.

                          Auxiliary definition: Multivariate polynomials in finitely many variables over an integral domain form an integral domain. This fact is proven by transport of structure from the MvPolynomial.noZeroDivisors_fin, and then used to prove the general case without finiteness hypotheses. See MvPolynomial.noZeroDivisors for the general case.

                          instance MvPolynomial.isDomain {R : Type u} {σ : Type v} [CommRing R] [IsDomain R] :

                          The multivariate polynomial ring over an integral domain is an integral domain.

                          Equations
                          • =
                          theorem MvPolynomial.map_mvPolynomial_eq_eval₂ {R : Type u} {σ : Type v} [CommRing R] {S : Type u_2} [CommRing S] [Finite σ] (ϕ : MvPolynomial σ R →+* S) (p : MvPolynomial σ R) :
                          ϕ p = MvPolynomial.eval₂ (ϕ.comp MvPolynomial.C) (fun (s : σ) => ϕ (MvPolynomial.X s)) p
                          theorem MvPolynomial.mem_ideal_of_coeff_mem_ideal {R : Type u} {σ : Type v} [CommRing R] (I : Ideal (MvPolynomial σ R)) (p : MvPolynomial σ R) (hcoe : ∀ (m : σ →₀ ), MvPolynomial.coeff m p Ideal.comap MvPolynomial.C I) :
                          p I

                          If every coefficient of a polynomial is in an ideal I, then so is the polynomial itself, multivariate version.

                          theorem MvPolynomial.mem_map_C_iff {R : Type u} {σ : Type v} [CommRing R] {I : Ideal R} {f : MvPolynomial σ R} :
                          f Ideal.map MvPolynomial.C I ∀ (m : σ →₀ ), MvPolynomial.coeff m f I

                          The push-forward of an ideal I of R to MvPolynomial σ R via inclusion is exactly the set of polynomials whose coefficients are in I

                          theorem MvPolynomial.ker_map {R : Type u} {S : Type u_1} {σ : Type v} [CommRing R] [CommRing S] (f : R →+* S) :
                          noncomputable def Polynomial.fintypeSubtypeMonicDvd {D : Type u} [CommRing D] [IsDomain D] [UniqueFactorizationMonoid D] (f : Polynomial D) (hf : f 0) :
                          Fintype { g : Polynomial D // g.Monic g f }

                          If D is a unique factorization domain, f is a non-zero polynomial in D[X], then f has only finitely many monic factors. (Note that its factors up to unit may be more than monic factors.) See also UniqueFactorizationMonoid.fintypeSubtypeDvd.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            theorem Polynomial.exists_monic_irreducible_factor {F : Type u_2} [Field F] (f : Polynomial F) (hu : ¬IsUnit f) :
                            ∃ (g : Polynomial F), g.Monic Irreducible g g f

                            A polynomial over a field which is not a unit must have a monic irreducible factor. See also WfDvdMonoid.exists_irreducible_factor.