isOpen_maximalIdeal

Mathlib.Topology.Algebra.Ring.Compact

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

English

In the same setting, the maximal ideal itself is an open subset of R.

Русский

В той же конфигурации максимальная идеал сама по себе является открытым подмножеством R.

LaTeX

$$$ IsOpen( maximalIdeal(R) ) $$$

Lean4

theorem isOpen_maximalIdeal : IsOpen (X := R) ↑(maximalIdeal R) :=
  Ideal.isOpen_of_isMaximal _

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

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

Разделы

Аффилиация

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