mathlib3 documentation


Quotients of polynomial rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

For a commutative ring $R$, evaluating a polynomial at an element $x \in R$ induces an isomorphism of $R$-algebras $R[X] / \langle X - x \rangle \cong R$.

theorem ideal.quotient_map_C_eq_zero {R : Type u_1} [comm_ring R] {I : ideal R} (a : R) (H : a I) :

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


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

theorem mv_polynomial.quotient_map_C_eq_zero {R : Type u_1} {σ : Type u_2} [comm_ring R] {I : ideal R} {i : R} (hi : i I) :