quotientSpanCXSubCXSubCAlgEquiv — Mathlib

English

If P is a prime ideal in R, then the quotient ring R[X] modulo the map of P is an integral domain.

Русский

Если P — простая идеал в R, то квотированное кольцо R[X] по этому идеалу является областью целых чисел.

LaTeX

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

Lean4

/-- For a commutative ring $R$, evaluating a polynomial at elements $y(X) \in R[X]$ and $x \in R$
induces an isomorphism of $R$-algebras $R[X, Y] / \langle X - x, Y - y(X) \rangle \cong R$. -/
noncomputable def quotientSpanCXSubCXSubCAlgEquiv {x : R} {y : R[X]} :
    @AlgEquiv R (R[X][X] ⧸ (Ideal.span {C (X - C x), X - C y} : Ideal <| R[X][X])) R _ _ _ (Ideal.Quotient.algebra R)
      _ :=
  ((quotientSpanCXSubCAlgEquiv (X - C x) y).restrictScalars R).trans <| quotientSpanXSubCAlgEquiv x

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