how to prove a vector space

Stream: general

[Blair Shi]

I want to prove vector_space F (has_space n F)and I have proved module F (has_space n F)

definition has_space (R : Type) (n : nat) := (fin n) → R

class vector_space (α : out_param $ Type u) (β : Type v) [field α] extends module α β

-- I want to show this one :(
instance (F : Type) (n : ℕ) [field F]: vector_space F (has_space F n) :=

[Mario Carneiro]

{}

[Blair Shi]

fair. thank you!

[Patrick Massot]

https://github.com/leanprover/mathlib/blob/7dc1f5d2dbda9dd412bb58636f4261bb259ad106/algebra/pi_instances.lean#L51

[Kevin Buzzard]

has_space F n is the finite-dimensional vector space F^n. What is a better name for this function?