Commit 2021-12-24 00:43 f03447fb
View on Github →feat(analysis/normed_space): a normed space over a nondiscrete normed field is noncompact (#10994)
Register this as an instance for a nondiscrete normed field and for a real normed vector space. Also add is_compact.ne_univ.