mathlib3

45d2b523 - chore(analysis/normed_space/basic): reorder the `restrict_scalars` definitions (#13995)

chore(analysis/normed_space/basic): reorder the `restrict_scalars` definitions (#13995) This also update the docstrings to make `normed_space.restrict_scalars` even scarier. The instances here themselves haven't actually changed.