mathlib3

daf01878 - chore(analysis/normed_space/basic): make `normed_space` extend `seminormed_space`

chore(analysis/normed_space/basic): make `normed_space` extend `seminormed_space` This saves a few lines, and is one step closer to eliminating the distinction between these two classes entirely