Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-24 09:35 53b79573

View on Github →

feat(analysis/normed_space/basic): if E is a normed_space over then ℤ ∙ e is discrete for any e in E (#16135)

Estimated changes