isField_of_isReduced

Mathlib.RingTheory.KrullDimension.Zero

URI: https://scilib.ai/kg/mathlib#Ring.KrullDimLE.isField_of_isReduced

← MathLib Explorer

English

If R is reduced and local, then R is a field.

Русский

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

LaTeX

$$[IsReduced R] & [IsLocalRing R] ⇒ IsField R$$

Lean4

theorem isField_of_isReduced [IsReduced R] [IsLocalRing R] : IsField R := by
  rw [IsLocalRing.isField_iff_maximalIdeal_eq, ← nilradical_eq_maximalIdeal, nilradical_eq_zero, Ideal.zero_eq_bot]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru