isOpen_of_isMaximal — Mathlib

English

In a compact Hausdorff ring, a maximal ideal I is open.

Русский

В компактном хаусдорфовом кольце максимальная идеал открыта.

LaTeX

$$IsOpen I$$

Lean4

theorem isOpen_of_isMaximal (I : Ideal R) [I.IsMaximal] : IsOpen (X := R) I :=
  have : I.toAddSubgroup.FiniteIndex :=
    @AddSubgroup.finiteIndex_of_finite_quotient _ _ _ (inferInstanceAs (Finite (R ⧸ I)))
  I.toAddSubgroup.isOpen_of_isClosed_of_finiteIndex (inferInstanceAs (IsClosed (X := R) I))

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