isDomain_map_C_quotient — Mathlib

English

If P is a prime ideal of R, then the quotient ring R[X] / map(C,P) is an integral domain.

Русский

Если P — простая идеал в R, то квотированное кольцо R[X] / map(C,P) является целой областью.

LaTeX

$$$P\\text{ prime }\\Rightarrow IsDomain\\bigl(R[X] / (\\operatorname{map} C P)\\bigr)$$$

Lean4

/-- If `P` is a prime ideal of `R`, then `R[x]/(P)` is an integral domain. -/
theorem isDomain_map_C_quotient {P : Ideal R} (_ : IsPrime P) :
    IsDomain (R[X] ⧸ (map (C : R →+* R[X]) P : Ideal R[X])) :=
  MulEquiv.isDomain (Polynomial (R ⧸ P)) (polynomialQuotientEquivQuotientPolynomial P).symm

Похожие утверждения