closure_eq — Mathlib

English

If I is a maximal ideal in a normed ring with summable geometric series, then I.closure = I.

Русский

Если I — максимальный идеал в нормированном кольце с суммируемой геометрической серией, то его замыкание равно самому I.

LaTeX

$$$I \\text{ maximal} \\Rightarrow \\overline{I} = I$$$

Lean4

/-- The `Ideal.closure` of a maximal ideal in a normed ring with summable
geometric series is the ideal itself. -/
theorem closure_eq {I : Ideal R} (hI : I.IsMaximal) : I.closure = I :=
  (hI.eq_of_le (I.closure_ne_top hI.ne_top) subset_closure).symm

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