Converting a Fin n → X to an ℕ →₀ X

Stream: Is there code for X?

[Niels Voss]

What is the best way to convert a Fin n → X finvec to a ℕ →₀ X? We have been using

import Mathlib
opaque n : ℕ
opaque f : Fin n → ℝ
noncomputable def g : ℕ →₀ ℝ := Finsupp.embDomain Fin.valEmbedding (Finsupp.ofSupportFinite f (Set.toFinite _))

but I would like to know if there is a better way.

[Yaël Dillies]

That looks okay to me!