Commit 2021-03-17 19:18 0b0fd528

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.