Topic: how to prove a vector space
Blair Shi (Aug 13 2018 at 10:23):
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 (Aug 13 2018 at 10:26):
Blair Shi (Aug 13 2018 at 10:29):
fair. thank you!
Patrick Massot (Aug 13 2018 at 10:39):
Kevin Buzzard (Aug 13 2018 at 10:53):
has_space F n is the finite-dimensional vector space F^n. What is a better name for this function?
Last updated: May 13 2021 at 05:21 UTC