isOpen_pow_of_isMaximal — Mathlib

English

For a maximal ideal I and any n, the n-th power I^n is open.

Русский

Для максимальной идеи I и любого n, I^n является открытым.

LaTeX

$$IsOpen (I^n)$$

Lean4

theorem isOpen_pow_of_isMaximal (I : Ideal R) [I.IsMaximal] (n : ℕ) : IsOpen (X := R) ↑(I ^ n) :=
  have : (I ^ n).toAddSubgroup.FiniteIndex :=
    @AddSubgroup.finiteIndex_of_finite_quotient _ _ _ (Ideal.finite_quotient_pow (IsNoetherian.noetherian _) _)
  (I ^ n).toAddSubgroup.isOpen_of_isClosed_of_finiteIndex (Ideal.isCompact_of_fg (IsNoetherian.noetherian _)).isClosed

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