Quotients of polynomial rings #
Equations
- Polynomial.quotientSpanXSubCAlgEquivAux2 x = { toEquiv := (RingHom.quotientKerEquivOfRightInverse ⋯).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
Instances For
Equations
Instances For
For a commutative ring
Equations
Instances For
For a commutative ring
Equations
- One or more equations did not get rendered due to their size.
Instances For
For a commutative ring
Equations
- One or more equations did not get rendered due to their size.
Instances For
If I
is an ideal of R
, then the ring polynomials over the quotient ring I.quotient
is
isomorphic to the quotient of R[X]
by the ideal map C I
,
where map C I
contains exactly the polynomials whose coefficients all lie in I
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If P
is a prime ideal of R
, then R[x]/(P)
is an integral domain.
Given any ring R
and an ideal I
of R[X]
, we get a map R → R[x] → R[x]/I
.
If we let R
be the image of R
in R[x]/I
then we also have a map R[x] → R'[x]
.
In particular we can map I
across this map, to get I'
and a new map R' → R'[x] → R'[x]/I
.
This theorem shows I'
will not contain any non-zero constant polynomials.
If I
is an ideal of R
, then the ring MvPolynomial σ I.quotient
is isomorphic as an
R
-algebra to the quotient of MvPolynomial σ R
by the ideal generated by I
.
Equations
- One or more equations did not get rendered due to their size.