Vectorization of Elements in Finite-Dimensional Vector Space

Stream: mathlib4

[Zichen Wang]

Suppose that

(F : Type) [NormedAddCommGroup F ] [InnerProductSpace ℝ F ] [FiniteDimensional ℝ F](b:F)

I now want to vectorize b, i.e. construct a mapping from an indicator set ( which size of is dimension of F) to each component of b. More specifically, I want to equate b to (Finset N \r Real),and I would like it to be derivable.Is there a better way of constructing it.
My solution is

variable {F : Type*}
[NormedAddCommGroup F ] [InnerProductSpace ℝ F ] [FiniteDimensional ℝ F]

lemma fin_to_F: Nonempty (Finset.range (FiniteDimensional.finrank ℝ F) ≃ (Basis.ofVectorSpaceIndex ℝ F)) := by
      refine Fintype.card_eq.mp ?_
      simp
      refine FiniteDimensional.finrank_eq_card_basis ?h
      exact Basis.extend _
def eqaute (b : F):= fun i =>
      (Basis.ofVectorSpace ℝ F).repr b ((Classical.choice fin_to_F) i)

[Eric Wieser]

Are you looking for docs#Module.finBasis ?

[Zichen Wang]

Thx.But what's a good way to convert between Finset.range n and Fin n?

[Zichen Wang]

Or between Fin n and Finset ℕ