# Documentation

Mathlib.RingTheory.Polynomial.Basic

# Ring-theoretic supplement of Data.Polynomial. #

## Main results #

• MvPolynomial.isDomain: If a ring is an integral domain, then so is its polynomial ring over finitely many variables.
• Polynomial.isNoetherianRing: Hilbert basis theorem, that if a ring is noetherian then so is its polynomial ring.
• Polynomial.wfDvdMonoid: If an integral domain is a WFDvdMonoid, then so is its polynomial ring.
• Polynomial.uniqueFactorizationMonoid, MvPolynomial.uniqueFactorizationMonoid: If an integral domain is a UniqueFactorizationMonoid, then so is its polynomial ring (of any number of variables).
def Polynomial.degreeLE (R : Type u) [] (n : ) :

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

Instances For
def Polynomial.degreeLT (R : Type u) [] (n : ) :

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

Instances For
theorem Polynomial.mem_degreeLE {R : Type u} [] {n : } {f : } :
f
theorem Polynomial.degreeLE_mono {R : Type u} [] {m : } {n : } (H : m n) :
theorem Polynomial.degreeLE_eq_span_X_pow {R : Type u} [] {n : } :
= Submodule.span R ↑(Finset.image (fun n => Polynomial.X ^ n) (Finset.range (n + 1)))
theorem Polynomial.mem_degreeLT {R : Type u} [] {n : } {f : } :
f
theorem Polynomial.degreeLT_mono {R : Type u} [] {m : } {n : } (H : m n) :
theorem Polynomial.degreeLT_eq_span_X_pow {R : Type u} [] {n : } :
= Submodule.span R ↑(Finset.image (fun n => Polynomial.X ^ n) ())
def Polynomial.degreeLTEquiv (R : Type u_2) [] (n : ) :
{ x // x } ≃ₗ[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} [] {n : } {p : } (hp : p ) :
↑() { val := p, property := hp } = 0 p = 0
theorem Polynomial.eval_eq_sum_degreeLTEquiv {R : Type u} [] {n : } {p : } (hp : p ) (x : R) :
= Finset.sum Finset.univ fun i => ↑() { val := p, property := hp } i * x ^ i
def Polynomial.frange {R : Type u} [] (p : ) :

The finset of nonzero coefficients of a polynomial.

Instances For
theorem Polynomial.frange_zero {R : Type u} [] :
theorem Polynomial.mem_frange_iff {R : Type u} [] {p : } {c : R} :
n, c =
theorem Polynomial.frange_one {R : Type u} [] :
{1}
theorem Polynomial.coeff_mem_frange {R : Type u} [] (p : ) (n : ) (h : 0) :
theorem Polynomial.geom_sum_X_comp_X_add_one_eq_sum {R : Type u} [] (n : ) :
Polynomial.comp (Finset.sum () fun i => Polynomial.X ^ i) (Polynomial.X + 1) = Finset.sum () fun i => ↑(Nat.choose n (i + 1)) * Polynomial.X ^ i
theorem Polynomial.Monic.geom_sum {R : Type u} [] {P : } (hP : ) (hdeg : ) {n : } (hn : n 0) :
Polynomial.Monic (Finset.sum () fun i => P ^ i)
theorem Polynomial.Monic.geom_sum' {R : Type u} [] {P : } (hP : ) (hdeg : ) {n : } (hn : n 0) :
Polynomial.Monic (Finset.sum () fun i => P ^ i)
theorem Polynomial.monic_geom_sum_X {R : Type u} [] {n : } (hn : n 0) :
Polynomial.Monic (Finset.sum () fun i => Polynomial.X ^ i)
def Polynomial.restriction {R : Type u} [Ring R] (p : ) :
Polynomial { x // }

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

Instances For
@[simp]
theorem Polynomial.coeff_restriction {R : Type u} [Ring R] {p : } {n : } :
↑() =
theorem Polynomial.coeff_restriction' {R : Type u} [Ring R] {p : } {n : } :
↑() =
@[simp]
theorem Polynomial.support_restriction {R : Type u} [Ring R] (p : ) :
@[simp]
theorem Polynomial.map_restriction {R : Type u} [] (p : ) :
Polynomial.map (algebraMap { x // } R) () = p
@[simp]
theorem Polynomial.degree_restriction {R : Type u} [Ring R] {p : } :
@[simp]
theorem Polynomial.natDegree_restriction {R : Type u} [Ring R] {p : } :
@[simp]
theorem Polynomial.monic_restriction {R : Type u} [Ring R] {p : } :
@[simp]
theorem Polynomial.restriction_zero {R : Type u} [Ring R] :
@[simp]
theorem Polynomial.restriction_one {R : Type u} [Ring R] :
theorem Polynomial.eval₂_restriction {R : Type u} {S : Type u_1} [Ring R] [] {f : R →+* S} {x : S} {p : } :
=
def Polynomial.toSubring {R : Type u} [Ring R] (p : ) (T : ) (hp : ↑() 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 : ) (T : ) (hp : ↑() T) {n : } :
↑(Polynomial.coeff () n) =
theorem Polynomial.coeff_toSubring' {R : Type u} [Ring R] (p : ) (T : ) (hp : ↑() T) {n : } :
↑(Polynomial.coeff () n) =
@[simp]
theorem Polynomial.support_toSubring {R : Type u} [Ring R] (p : ) (T : ) (hp : ↑() T) :
@[simp]
theorem Polynomial.degree_toSubring {R : Type u} [Ring R] (p : ) (T : ) (hp : ↑() T) :
@[simp]
theorem Polynomial.natDegree_toSubring {R : Type u} [Ring R] (p : ) (T : ) (hp : ↑() T) :
@[simp]
theorem Polynomial.monic_toSubring {R : Type u} [Ring R] (p : ) (T : ) (hp : ↑() T) :
@[simp]
theorem Polynomial.toSubring_zero {R : Type u} [Ring R] (T : ) :
Polynomial.toSubring 0 T (_ : T) = 0
@[simp]
theorem Polynomial.toSubring_one {R : Type u} [Ring R] (T : ) :
Polynomial.toSubring 1 T (_ : ↑() T) = 1
@[simp]
theorem Polynomial.map_toSubring {R : Type u} [Ring R] (p : ) (T : ) (hp : ↑() T) :
def Polynomial.ofSubring {R : Type u} [Ring R] (T : ) (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 : ) (p : Polynomial { x // x T }) (n : ) :
= ↑()
@[simp]
theorem Polynomial.frange_ofSubring {R : Type u} [Ring R] (T : ) {p : Polynomial { x // x T }} :
↑() T
theorem Polynomial.mem_ker_modByMonic {R : Type u} [] {q : } (hq : ) {p : } :
q p
@[simp]
theorem Polynomial.ker_modByMonicHom {R : Type u} [] {q : } (hq : ) :
def Ideal.ofPolynomial {R : Type u} [] (I : Ideal ()) :

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

Instances For
theorem Ideal.mem_ofPolynomial {R : Type u} [] {I : Ideal ()} (x : ) :
x I
def Ideal.degreeLE {R : Type u} [] (I : Ideal ()) (n : ) :

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} [] (I : Ideal ()) (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} [] (I : Ideal ()) :

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} [] (I : Ideal ()) (p : ) (hp : ∀ (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} [] {I : } {f : } :
f Ideal.map Polynomial.C I ∀ (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} [] [] (f : R →+* S) :
= Ideal.map Polynomial.C ()
theorem Ideal.mem_leadingCoeffNth {R : Type u} [] (I : Ideal ()) (n : ) (x : R) :
p, p I
theorem Ideal.mem_leadingCoeffNth_zero {R : Type u} [] (I : Ideal ()) (x : R) :
Polynomial.C x I
theorem Ideal.leadingCoeffNth_mono {R : Type u} [] (I : Ideal ()) {m : } {n : } (H : m n) :
theorem Ideal.mem_leadingCoeff {R : Type u} [] (I : Ideal ()) (x : R) :
p, p I
theorem Polynomial.coeff_prod_mem_ideal_pow_tsub {R : Type u} [] {ι : Type u_2} (s : ) (f : ι) (I : ) (n : ι) (h : ∀ (i : ι), i s∀ (k : ), Polynomial.coeff (f i) k I ^ (n i - k)) (k : ) :
Polynomial.coeff () k I ^ ( - 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 : ) (I : Ideal ()) [hI : ] (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} [] (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 Ideal.isPrime_map_C_of_isPrime {R : Type u} [] {P : } (H : ) :
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 Ideal.is_fg_degreeLE {R : Type u} [] [] (I : Ideal ()) (n : ) :
theorem Polynomial.prime_C_iff {R : Type u} [] {r : R} :
Prime (Polynomial.C r)
theorem MvPolynomial.prime_C_iff {R : Type u} (σ : Type v) [] {r : R} :
Prime (MvPolynomial.C r)
theorem MvPolynomial.prime_rename_iff {R : Type u} {σ : Type v} [] (s : Set σ) {p : MvPolynomial (s) R} :
Prime (↑(MvPolynomial.rename Subtype.val) p)
theorem Polynomial.isNoetherianRing {R : Type u} [] [inst : ] :

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

theorem Polynomial.exists_irreducible_of_degree_pos {R : Type u} [] [] [] {f : } (hf : ) :
g, g f
theorem Polynomial.exists_irreducible_of_natDegree_pos {R : Type u} [] [] [] {f : } (hf : ) :
g, g f
theorem Polynomial.exists_irreducible_of_natDegree_ne_zero {R : Type u} [] [] [] {f : } (hf : ) :
g, g f
theorem Polynomial.linearIndependent_powers_iff_aeval {R : Type u} {M : Type w} [] [] [Module R M] (f : M →ₗ[R] M) (v : M) :
(LinearIndependent R fun n => ↑(f ^ n) v) ∀ (p : ), ↑(↑() p) v = 0p = 0
theorem Polynomial.disjoint_ker_aeval_of_coprime {R : Type u} {M : Type w} [] [] [Module R M] (f : M →ₗ[R] M) {p : } {q : } (hpq : ) :
Disjoint (LinearMap.ker (↑() p)) (LinearMap.ker (↑() q))
theorem Polynomial.sup_aeval_range_eq_top_of_coprime {R : Type u} {M : Type w} [] [] [Module R M] (f : M →ₗ[R] M) {p : } {q : } (hpq : ) :
theorem Polynomial.sup_ker_aeval_le_ker_aeval_mul {R : Type u} {M : Type w} [] [] [Module R M] {f : M →ₗ[R] M} {p : } {q : } :
LinearMap.ker (↑() p) LinearMap.ker (↑() q) LinearMap.ker (↑() (p * q))
theorem Polynomial.sup_ker_aeval_eq_ker_aeval_mul_of_coprime {R : Type u} {M : Type w} [] [] [Module R M] (f : M →ₗ[R] M) {p : } {q : } (hpq : ) :
LinearMap.ker (↑() p) LinearMap.ker (↑() q) = LinearMap.ker (↑() (p * q))
instance MvPolynomial.isNoetherianRing {R : Type u} {σ : Type v} [] [] [] :

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.

theorem MvPolynomial.noZeroDivisors_of_finite (R : Type u) (σ : Type v) [] [] [] :

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} [] {S : Type u_2} [] [] (ϕ : →+* S) (p : ) :
ϕ p = MvPolynomial.eval₂ (RingHom.comp ϕ MvPolynomial.C) (fun s => ϕ ()) p
theorem MvPolynomial.mem_ideal_of_coeff_mem_ideal {R : Type u} {σ : Type v} [] (I : Ideal ()) (p : ) (hcoe : ∀ (m : σ →₀ ), 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} [] {I : } {f : } :
f Ideal.map MvPolynomial.C I ∀ (m : σ →₀ ), 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} [] [] (f : R →+* S) :
= Ideal.map MvPolynomial.C ()