mathlib

91b87d4f - chore(analysis/normed_space/basic): reorder `restrict_scalars.normed_space` and `normed_space.restrict_scalars`

chore(analysis/normed_space/basic): reorder `restrict_scalars.normed_space` and `normed_space.restrict_scalars` The former is the `instance` on `restrict_scalars`, the latter is the scary `def` that warrants the warning message and does not use a type synonym. This changes all the call sites to use the `def` too.