isField_of_isReduced_of_isLocalRing

English

Let R be a commutative Artinian ring. If R is reduced and local, then R is a field.

Русский

Пусть R — коммутативное артинианово кольцо. Если R редуктировано и локально, то R — поле.

LaTeX

$$$ [IsReduced\ R] \land [IsLocalRing\ R] \Rightarrow IsField\ R $$$

Lean4

/-- Commutative Artinian reduced local ring is a field. -/
theorem isField_of_isReduced_of_isLocalRing [IsReduced R] [IsLocalRing R] : IsField R :=
  (IsArtinianRing.equivPi R).trans (RingEquiv.piUnique _) |>.toMulEquiv.isField (Ideal.Quotient.field _).toIsField

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