Documentation

Mathlib.RingTheory.Polynomial.Basic

Ring-theoretic supplement of Data.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.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.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.degreeLTEquiv_eq_zero_iff_eq_zero {R : Type u} [Semiring R] {n : } {p : Polynomial R} (hp : p Polynomial.degreeLT R n) :
        (Polynomial.degreeLTEquiv R n) { val := p, property := hp } = 0 p = 0
        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 = Finset.sum Finset.univ fun (i : Fin n) => (Polynomial.degreeLTEquiv R n) { val := p, property := hp } i * x ^ i

        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.

        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 : Set.Finite s) :

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

        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.frange {R : Type u} [Semiring R] (p : Polynomial R) :

        The finset of nonzero coefficients of a polynomial.

        Equations
        Instances For
          theorem Polynomial.geom_sum_X_comp_X_add_one_eq_sum {R : Type u} [Semiring R] (n : ) :
          Polynomial.comp (Finset.sum (Finset.range n) fun (i : ) => Polynomial.X ^ i) (Polynomial.X + 1) = Finset.sum (Finset.range n) fun (i : ) => (Nat.choose n (i + 1)) * Polynomial.X ^ i
          theorem Polynomial.Monic.geom_sum {R : Type u} [Semiring R] {P : Polynomial R} (hP : Polynomial.Monic P) (hdeg : 0 < Polynomial.natDegree P) {n : } (hn : n 0) :
          theorem Polynomial.Monic.geom_sum' {R : Type u} [Semiring R] {P : Polynomial R} (hP : Polynomial.Monic P) (hdeg : 0 < Polynomial.degree P) {n : } (hn : n 0) :
          theorem Polynomial.monic_geom_sum_X {R : Type u} [Semiring R] {n : } (hn : n 0) :
          Polynomial.Monic (Finset.sum (Finset.range n) fun (i : ) => Polynomial.X ^ i)

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

          Equations
          Instances For
            def Polynomial.toSubring {R : Type u} [Ring R] (p : Polynomial R) (T : Subring R) (hp : (Polynomial.frange p) 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 : (Polynomial.frange p) T) {n : } :
              theorem Polynomial.coeff_toSubring' {R : Type u} [Ring R] (p : Polynomial R) (T : Subring R) (hp : (Polynomial.frange p) T) {n : } :
              @[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 : (Polynomial.frange p) T) :
              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
                @[simp]
                theorem Polynomial.frange_ofSubring {R : Type u} [Ring R] (T : Subring R) {p : Polynomial T} :

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

                Equations
                • Ideal.ofPolynomial I = { toAddSubmonoid := { toAddSubsemigroup := { carrier := I.carrier, add_mem' := }, zero_mem' := }, smul_mem' := }
                Instances For
                  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
                      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 : ), Polynomial.coeff p 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 : ), Polynomial.coeff f 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 Ideal.mem_leadingCoeffNth_zero {R : Type u} [CommSemiring R] (I : Ideal (Polynomial R)) (x : R) :
                        x Ideal.leadingCoeffNth I 0 Polynomial.C x I
                        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 : ), Polynomial.coeff (f i) k I ^ (n i - k)) (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 : Ideal.IsMaximal I] (x : R) (hx : Polynomial.C x I) :
                        x = 0

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

                        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 : Ideal.IsPrime P) :
                        Ideal.IsPrime (Ideal.map Polynomial.C P)

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

                        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
                        Equations
                        • =

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

                        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 : MvPolynomial.totalDegree F m) (f : σPolynomial R) (hf : ∀ (i : σ), Polynomial.natDegree (f i) 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₂ (RingHom.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) :

                        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

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