closure_ne_top — Mathlib

English

If I is a proper ideal in a normed ring with summable geometric series, then its closure I.closure is also proper.

Русский

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

LaTeX

$$$I \\neq R \\Rightarrow \\overline{I} \\neq R$$$

Lean4

/-- The `Ideal.closure` of a proper ideal in a normed ring with summable
geometric series is proper. -/
theorem closure_ne_top (I : Ideal R) (hI : I ≠ ⊤) : I.closure ≠ ⊤ :=
  by
  have h := closure_minimal (coe_subset_nonunits hI) nonunits.isClosed
  simpa only [I.closure.eq_top_iff_one, Ne] using mt (@h 1) one_notMem_nonunits

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