How to get EuclideanSpace Real (Fin n) from Fin n -> Real?

Stream: new members

[Ilmārs Cīrulis]

Hello! I have yet another beginner's question. :sweat_smile:

Let's suppose I have some function of type Fin n → ℝ... how can I coerce (?) it to EuclideanSpace ℝ (Fin n)?

Thank you!

[Eric Wieser]

docs#WithLp.equiv .symm

[Ilmārs Cīrulis]

Thank you very much! :)