Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ideal.is_maximal.closure_eq

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.is_maximal.closure_eq View on Github →