nilradical_eq_maximalIdeal

Mathlib.RingTheory.KrullDimension.Zero

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

← MathLib Explorer

English

In a local ring R, the nilradical equals the maximal ideal.

Русский

В локальном кольце R нильрадикал равен максимальному идеалу.

LaTeX

$$nilradical(R) = maximalIdeal(R)$$

Lean4

theorem nilradical_eq_maximalIdeal [IsLocalRing R] : nilradical R = IsLocalRing.maximalIdeal R :=
  Ideal.ext fun _ ↦ isNilpotent_iff_mem_maximalIdeal

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

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

Разделы

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

Аффилиация

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