finite domain -> finsupp

Stream: Is there code for X?

[Joseph Hua]

I'm wondering if there's already something for

/-- converts map from fin n to same map with finite support -/
def finsupp_of_fin_dom {A : Type*} [has_zero A] {n : ℕ}
  (f : fin n → A) :
  fin n →₀ A :=
finsupp.on_finset finset.univ f (λ a h, finset.mem_univ _)

I guess his could be more generally for a map from a fintype?

[Eric Wieser]

docs#finsupp.equiv_fun_on_fintype

[Joseph Hua]

yay thanks!