instIsHausdorffMaximalIdeal

Mathlib.RingTheory.AdicCompletion.Noetherian

URI: https://scilib.ai/kg/mathlib#instIsHausdorffMaximalIdeal

English

If R is a local ring, then IsHausdorff (maximalIdeal R) M holds for any M.

Русский

Если R локальное кольцо, то IsHausdorff (maximalIdeal R) M выполняется для любого M.

LaTeX

$$$\text{IsHausdorff} (\text{maximalIdeal } R)\ M$$$

Lean4

instance [IsLocalRing R] : IsHausdorff (maximalIdeal R) M :=
  .of_le_jacobson _ _ (maximalIdeal_le_jacobson _)

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

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

Разделы

Аффилиация

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