FunLike instance for EuclideanSpace

Stream: mathlib4

[Jireh Loreaux]

Should we give docs#EuclideanSpace and/or docs#WithLp a FunLike instance? Would it even be effective? As it is, it's pretty annoying to work with matrices and these types (especially around Matrix.mulVec) because it's hard not to break the defeq barrier of EuclideanSpace 𝕜 n and n → 𝕜.

[Yaël Dillies]

You can try but I believe unfolding EuclideanSpace/WithLp takes priority over looking for a FunLike instance, so your solution would be ineffective.

[Jireh Loreaux]

That's what I feared.