EuclideanSpace.single as continuous linear map

Stream: new members

[Ben Eltschig]

I'm currently computing something related to derivates of paths, and for that want to refer to $f : \mathbb R\to\mathbb R^1,t\mapsto(t)$ as a continuous linear map. As far as I can tell this should be EuclideanSpace.single (0 : Fin 1), but unlike EuclideanSpace.proj i that hasn't been registered as a continuous linear map yet, only as a simple function. Is that intentional, or is it just because no one needed it as a continuous linear map yet? If it's the latter, could that be a good first PR?