of_isPrincipalIdealRing_polynomial

English

If R is a domain and R[X] is a principal ideal ring, then R is a field.

Русский

Если R — домен и R[X] — кольцо главных идеалов, то R — поле.

LaTeX

$$$[IsDomain R] \\land [IsPrincipalIdealRing (R[X])] \\Rightarrow IsField R$$$

Lean4

/-- Given a domain `R`, if `R[X]` is a principal ideal ring, then `R` is a field. -/
theorem of_isPrincipalIdealRing_polynomial [IsDomain R] [IsPrincipalIdealRing R[X]] : IsField R :=
  by
  apply (quotientSpanXSubCAlgEquiv 0).symm.toMulEquiv.isField
  rw [← Quotient.maximal_ideal_iff_isField_quotient]
  exact PrincipalIdealRing.isMaximal_of_irreducible (irreducible_X_sub_C 0)

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