Zulip Chat Archive

Stream: general

Topic: how to prove a vector space


view this post on Zulip 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) :=

view this post on Zulip Mario Carneiro (Aug 13 2018 at 10:26):

{}

view this post on Zulip Blair Shi (Aug 13 2018 at 10:29):

fair. thank you!

view this post on Zulip Patrick Massot (Aug 13 2018 at 10:39):

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

view this post on Zulip 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