Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nonunits.subset_compl_ball

Modification history

2022-09-13 06:29

src/analysis/normed_space/units.lean

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

Added nonunits.subset_compl_ball View on Github →