mathlib3

f03447fb - feat(analysis/normed_space): a normed space over a nondiscrete normed field is noncompact (#10994)

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`.