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

Commit

3 years ago

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

Author

ocfnash

Parents