isOpen_maximalIdeal_pow — Mathlib

English

In the same setting, for each natural number n, the n-th power of the maximal ideal is an open subset of R.

Русский

В той же ситуации для каждого натурального числа n мощность максимальной идеалы I^n является открытым подмножеством R.

LaTeX

$$$\\forall n \\in \\mathbb{N}, \\ IsOpen( (maximalIdeal(R))^n )$$$

Lean4

theorem isOpen_maximalIdeal_pow (n : ℕ) : IsOpen (X := R) ↑(maximalIdeal R ^ n) :=
  Ideal.isOpen_pow_of_isMaximal _ _

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