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.





leanprover-community/mathlib,leanprover-community/mathlib