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)
feat(analysis/normed_space/basic): if E is a normed_space over ℚ then ℤ ∙ e is discrete for any e in E (#16135)