mathlib

ce26d75d - refactor(analysis/normed_space/basic): split into normed_space and ../normed/normed_field (#12410)

refactor(analysis/normed_space/basic): split into normed_space and ../normed/normed_field (#12410) Splits off the sections about normed rings and fields of the file `analysis/normed_space/basic` into a new file `analysis/normed/normed_field`.