Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ideal.closure_ne_top

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 ideal.closure_ne_top View on Github →