of_isMaximal_nilradical

Mathlib.RingTheory.KrullDimension.Zero

URI: https://scilib.ai/kg/mathlib#IsLocalRing.of_isMaximal_nilradical

← MathLib Explorer

English

If the nilradical is maximal, then the Krull dimension of 0 is nonpositive.

Русский

Если нильрадикал максимален, то размер Крull кольца не более нуля.

LaTeX

$$nilradical(R).IsMaximal ⇒ Ring.KrullDimLE 0 R$$

Lean4

theorem of_isMaximal_nilradical [(nilradical R).IsMaximal] : IsLocalRing R :=
  (((Ring.krullDimLE_zero_and_isLocalRing_tfae R).out 3 0 rfl rfl).mp ‹_›).2

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

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

Разделы

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

Аффилиация

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