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 aWFDvdMonoid
, then so is its polynomial ring.Polynomial.uniqueFactorizationMonoid
,MvPolynomial.uniqueFactorizationMonoid
: If an integral domain is aUniqueFactorizationMonoid
, then so is its polynomial ring (of any number of variables).
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
The finset of nonzero coefficients of a polynomial.
Instances For
Given a polynomial, return the polynomial whose coefficients are in the ring closure of the original coefficients.
Instances For
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
Given a polynomial whose coefficients are in some subring, return the corresponding polynomial whose coefficients are in the ambient ring.
Instances For
Transport an ideal of R[X]
to an R
-submodule of R[X]
.
Instances For
Given an ideal I
of R[X]
, make the R
-submodule of I
consisting of polynomials of degree ≤ n
.
Instances For
Given an ideal I
of R[X]
, make the ideal in R
of
leading coefficients of polynomials in I
with degree ≤ n
.
Instances For
Given an ideal I
in R[X]
, make the ideal in R
of the
leading coefficients in I
.
Instances For
If every coefficient of a polynomial is in an ideal I
, then so is the polynomial itself
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
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
.
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]
.
If P
is a prime ideal of R
, then P.R[x]
is a prime ideal of R[x]
.
Hilbert basis theorem: a polynomial ring over a noetherian ring is a noetherian ring.
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.
If every coefficient of a polynomial is in an ideal I
, then so is the polynomial itself,
multivariate version.
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