# Ring-theoretic supplement of Algebra.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).
instance Polynomial.instCharP {R : Type u} [] (p : ) [h : CharP R p] :
CharP () p
Equations
• =
instance Polynomial.instExpChar {R : Type u} [] (p : ) [h : ExpChar R p] :
ExpChar () p
Equations
• =
def Polynomial.degreeLE (R : Type u) [] (n : ) :

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

Equations
• = ⨅ (k : ), ⨅ (_ : k > n),
Instances For
def Polynomial.degreeLT (R : Type u) [] (n : ) :

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

Equations
• = ⨅ (k : ), ⨅ (_ : k n),
Instances For
theorem Polynomial.mem_degreeLE {R : Type u} [] {n : } {f : } :
f f.degree n
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 f.degree < n
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 : ) :
() ≃ₗ[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} [] {n : } {p : } (hp : p ) :
() p, hp = 0 p = 0
theorem Polynomial.eval_eq_sum_degreeLTEquiv {R : Type u} [] {n : } {p : } (hp : p ) (x : R) :
= i : Fin n, () p, hp i * x ^ i
theorem Polynomial.exists_degree_le_of_mem_span {R : Type u} [] {s : Set ()} {p : } (hs : s.Nonempty) (hp : p ) :
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} [] {s : Set ()} (s_fin : s.Finite) (hs : s.Nonempty) :
p's, p, 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} [] {s : Set ()} (s_fin : s.Finite) :
∃ (n : ),

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} [] {s : Set ()} (s_fin : s.Finite) :
∃ (n : ),

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

theorem Polynomial.not_finite {R : Type u} [] [] :

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

The finset of nonzero coefficients of a polynomial.

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

Alias of Polynomial.coeffs.

The finset of nonzero coefficients of a polynomial.

Equations
Instances For
theorem Polynomial.coeffs_zero {R : Type u} [] :
@[deprecated Polynomial.coeffs_zero]
theorem Polynomial.frange_zero {R : Type u} [] :

Alias of Polynomial.coeffs_zero.

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

Alias of Polynomial.mem_coeffs_iff.

theorem Polynomial.coeffs_one {R : Type u} [] :
{1}
@[deprecated Polynomial.coeffs_one]
theorem Polynomial.frange_one {R : Type u} [] :
{1}

Alias of Polynomial.coeffs_one.

theorem Polynomial.coeff_mem_coeffs {R : Type u} [] (p : ) (n : ) (h : p.coeff n 0) :
p.coeff n p.coeffs
@[deprecated Polynomial.coeff_mem_coeffs]
theorem Polynomial.coeff_mem_frange {R : Type u} [] (p : ) (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} [] (n : ) :
(i, Polynomial.X ^ i).comp (Polynomial.X + 1) = i, (n.choose (i + 1)) * Polynomial.X ^ i
theorem Polynomial.Monic.geom_sum {R : Type u} [] {P : } (hP : P.Monic) (hdeg : 0 < P.natDegree) {n : } (hn : n 0) :
(i, P ^ i).Monic
theorem Polynomial.Monic.geom_sum' {R : Type u} [] {P : } (hP : P.Monic) (hdeg : 0 < P.degree) {n : } (hn : n 0) :
(i, P ^ i).Monic
theorem Polynomial.monic_geom_sum_X {R : Type u} [] {n : } (hn : n 0) :
(i, Polynomial.X ^ i).Monic
def Polynomial.restriction {R : Type u} [Ring R] (p : ) :
Polynomial (Subring.closure p.coeffs)

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

Equations
• p.restriction = ip.support, p.coeff i,
Instances For
@[simp]
theorem Polynomial.coeff_restriction {R : Type u} [Ring R] {p : } {n : } :
(p.restriction.coeff n) = p.coeff n
theorem Polynomial.coeff_restriction' {R : Type u} [Ring R] {p : } {n : } :
(p.restriction.coeff n) = p.coeff n
@[simp]
theorem Polynomial.support_restriction {R : Type u} [Ring R] (p : ) :
p.restriction.support = p.support
@[simp]
theorem Polynomial.map_restriction {R : Type u} [] (p : ) :
Polynomial.map (algebraMap ((Subring.closure p.coeffs)) R) p.restriction = p
@[simp]
theorem Polynomial.degree_restriction {R : Type u} [Ring R] {p : } :
p.restriction.degree = p.degree
@[simp]
theorem Polynomial.natDegree_restriction {R : Type u} [Ring R] {p : } :
p.restriction.natDegree = p.natDegree
@[simp]
theorem Polynomial.monic_restriction {R : Type u} [Ring R] {p : } :
p.restriction.Monic p.Monic
@[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 : } :
= Polynomial.eval₂ (f.comp (Subring.closure p.coeffs).subtype) x p.restriction
def Polynomial.toSubring {R : Type u} [Ring R] (p : ) (T : ) (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
• p.toSubring T hp = ip.support, p.coeff i,
Instances For
@[simp]
theorem Polynomial.coeff_toSubring {R : Type u} [Ring R] (p : ) (T : ) (hp : p.coeffs T) {n : } :
((p.toSubring T hp).coeff n) = p.coeff n
theorem Polynomial.coeff_toSubring' {R : Type u} [Ring R] (p : ) (T : ) (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 : ) (T : ) (hp : p.coeffs T) :
(p.toSubring T hp).support = p.support
@[simp]
theorem Polynomial.degree_toSubring {R : Type u} [Ring R] (p : ) (T : ) (hp : p.coeffs T) :
(p.toSubring T hp).degree = p.degree
@[simp]
theorem Polynomial.natDegree_toSubring {R : Type u} [Ring R] (p : ) (T : ) (hp : p.coeffs T) :
(p.toSubring T hp).natDegree = p.natDegree
@[simp]
theorem Polynomial.monic_toSubring {R : Type u} [Ring R] (p : ) (T : ) (hp : p.coeffs T) :
(p.toSubring T hp).Monic p.Monic
@[simp]
theorem Polynomial.toSubring_zero {R : Type u} [Ring R] (T : ) :
= 0
@[simp]
theorem Polynomial.toSubring_one {R : Type u} [Ring R] (T : ) :
= 1
@[simp]
theorem Polynomial.map_toSubring {R : Type u} [Ring R] (p : ) (T : ) (hp : p.coeffs T) :
Polynomial.map T.subtype (p.toSubring T hp) = p
def Polynomial.ofSubring {R : Type u} [Ring R] (T : ) (p : ) :

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

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

Alias of Polynomial.coeffs_ofSubring.

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

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

Equations
• I.degreeLE n = I.ofPolynomial
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.

Equations
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.

Equations
Instances For
theorem Ideal.polynomial_mem_ideal_of_coeff_mem_ideal {R : Type u} [] (I : Ideal ()) (p : ) (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} [] {I : } {f : } :
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} [] [] (f : R →+* S) :
LinearMap.ker .toSemilinearMap = Ideal.map Polynomial.C ()
theorem Ideal.mem_leadingCoeffNth {R : Type u} [] (I : Ideal ()) (n : ) (x : R) :
theorem Ideal.mem_leadingCoeffNth_zero {R : Type u} [] (I : Ideal ()) (x : R) :
x I.leadingCoeffNth 0 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) :
theorem Polynomial.coeff_prod_mem_ideal_pow_tsub {R : Type u} [] {ι : Type u_2} (s : ) (f : ι) (I : ) (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 : ) (I : Ideal ()) [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} [] (P : ) :
(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} [] {P : } (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} [] [] (I : Ideal ()) (n : ) :
(I.degreeLE n).FG
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)
@[instance 100]
instance Polynomial.wfDvdMonoid {R : Type u_2} [] [] [] :
Equations
• =
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 : 0 < f.degree) :
∃ (g : ), g f
theorem Polynomial.exists_irreducible_of_natDegree_pos {R : Type u} [] [] [] {f : } (hf : 0 < f.natDegree) :
∃ (g : ), g f
theorem Polynomial.exists_irreducible_of_natDegree_ne_zero {R : Type u} [] [] [] {f : } (hf : f.natDegree 0) :
∃ (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 : ) :
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 : } :
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))
theorem MvPolynomial.aeval_natDegree_le {σ : Type v} {R : Type u_2} [] {m : } {n : } (F : ) (hF : F.totalDegree m) (f : σ) (hf : ∀ (i : σ), (f i).natDegree n) :
( F).natDegree m * n
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.

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.

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.

instance MvPolynomial.instNoZeroDivisors {R : Type u} [] [] {σ : Type v} :
Equations
• =
instance MvPolynomial.isDomain {R : Type u} {σ : Type v} [] [] :

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

Equations
• =
theorem MvPolynomial.map_mvPolynomial_eq_eval₂ {R : Type u} {σ : Type v} [] {S : Type u_2} [] [] (ϕ : →+* S) (p : ) :
ϕ p = MvPolynomial.eval₂ (ϕ.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 ()
@[instance 100]
Equations
• =
noncomputable def Polynomial.fintypeSubtypeMonicDvd {D : Type u} [] [] (f : ) (hf : f 0) :
Fintype { g : // 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
@[instance 100]
instance MvPolynomial.uniqueFactorizationMonoid (σ : Type v) {D : Type u} [] [] :
Equations
• =
theorem Polynomial.exists_monic_irreducible_factor {F : Type u_2} [] (f : ) (hu : ¬) :
∃ (g : ), g.Monic g f

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