# mathlib3documentation

ring_theory.polynomial.quotient

# Quotients of polynomial rings #

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

noncomputable def polynomial.quotient_span_X_sub_C_alg_equiv {R : Type u_1} [comm_ring R] (x : R) :

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

Equations
@[simp]
theorem polynomial.quotient_span_X_sub_C_alg_equiv_mk {R : Type u_1} [comm_ring R] (x : R) (p : polynomial R) :
@[simp]
noncomputable def polynomial.quotient_span_C_X_sub_C_alg_equiv {R : Type u_1} [comm_ring R] (x y : R) :

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

Equations
theorem ideal.quotient_map_C_eq_zero {R : Type u_1} [comm_ring R] {I : ideal R} (a : R) (H : a I) :
= 0
theorem ideal.eval₂_C_mk_eq_zero {R : Type u_1} [comm_ring R] {I : ideal R} (f : polynomial R) (H : f ) :

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
theorem ideal.is_domain_map_C_quotient {R : Type u_1} [comm_ring R] {P : ideal R} (H : P.is_prime) :

If P is a prime ideal of R, then R[x]/(P) is an integral domain.

theorem ideal.eq_zero_of_polynomial_mem_map_range {R : Type u_1} [comm_ring R] (I : ideal (polynomial R)) (x : .range))  :
x = 0

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) :
theorem mv_polynomial.eval₂_C_mk_eq_zero {R : Type u_1} {σ : Type u_2} [comm_ring R] {I : ideal R} {a : R} (ha : a ) :
noncomputable def mv_polynomial.quotient_equiv_quotient_mv_polynomial {R : Type u_1} {σ : Type u_2} [comm_ring R] (I : ideal R) :
(R I) ≃ₐ[R]

If I is an ideal of R, then the ring mv_polynomial σ I.quotient is isomorphic as an R-algebra to the quotient of mv_polynomial σ R by the ideal generated by I.

Equations