mathlib3

294e445b - chore(analysis/normed_space/real): separate results about real normed spaces