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)