Documentation

Mathlib.RingTheory.Polynomial.Basic

Ring-theoretic supplement of Data.Polynomial. #

Main results #

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

Instances For

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

    Instances For
      theorem Polynomial.degreeLE_eq_span_X_pow {R : Type u} [Semiring 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] {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 : ) :
      { x // x Polynomial.degreeLT R n } ≃ₗ[R] Fin nR

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

      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 => ↑(Polynomial.degreeLTEquiv R n) { val := p, property := hp } i * x ^ i
        def Polynomial.frange {R : Type u} [Semiring R] (p : Polynomial R) :

        The finset of nonzero coefficients of a polynomial.

        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.

          Instances For
            def Polynomial.toSubring {R : Type u} [Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑(Polynomial.frange p) T) :
            Polynomial { x // x T }

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

            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) :
              Polynomial.toSubring 0 T (_ : T) = 0
              @[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 { x // x T }) :

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

              Instances For
                theorem Polynomial.coeff_ofSubring {R : Type u} [Ring R] (T : Subring R) (p : Polynomial { x // x T }) (n : ) :
                @[simp]
                theorem Polynomial.frange_ofSubring {R : Type u} [Ring R] (T : Subring R) {p : Polynomial { x // x T }} :

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

                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.

                  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.

                    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.

                      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 : ∀ (i : ι), i s∀ (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

                        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

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

                        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.

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

                        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) :