mathlib

0b0fd528 - chore(analysis/normed_space/extend): provide a version without restrict_scalars (#6693)

chore(analysis/normed_space/extend): provide a version without restrict_scalars (#6693) This is some pre-work to try and speed up the proof in `hahn_banach`, which as I understand it is super slow because it has to work very hard to unify typeclass which keep switching back and forth between `F` and `restrict_scalars ℝ 𝕜 F`. This PR is unlikely to have changed the speed of that proof, but I suspect these definitions might help in a future PR - and it pushes `restrict_scalars` out of the interesting bit of the proof.