Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-13 06:29 4ff10212

View on Github →

feat(analysis/normed_space/units): maximal ideals in complete normed rings are closed (#16303)

Estimated changes

Modified src/analysis/normed_space/units.lean

added theorem ideal.closure_ne_top

added theorem ideal.eq_top_of_norm_lt_one

added theorem ideal.is_maximal.closure_eq

added theorem nonunits.subset_compl_ball

Modified src/topology/algebra/ring.lean