Stream: new members
Topic: vector spaces
bumby bumby (Apr 09 2021 at 14:24):
hi i m new in lean i m reading mathematics in lean, what libraries can i use to prove general vector spaces or if a set is a vector space? because in the book explains for rings but i see those are little different that vector spaces
Anne Baanen (Apr 09 2021 at 14:33):
Hi, welcome! We have a quick tour through the linear algebra library of mathlib here: https://leanprover-community.github.io/theories/linear_algebra.html
So I understand your question as: "I have a set V along with some operations
•, how can I show this is a vector space?"
Kevin Buzzard (Apr 09 2021 at 14:33):
A "thing" isn't a vector space by itself, you have to make it a vector space by defining stuff like addition and multiplication. I think this conversation would be easier if we focussed on a much more precise question.
Eric Wieser (Apr 09 2021 at 14:36):
Anne Baanen (Apr 09 2021 at 14:37):
Or maybe docs#submodule since we're starting with a set.
bumby bumby (Apr 09 2021 at 15:05):
Johan Commelin (Apr 09 2021 at 15:09):
@bumby bumby Have you played the natural number game? It's a great way to get started with Lean.
bumby bumby (Apr 09 2021 at 15:10):
i started reading mathematics_in_lean and is great i started prove small theorems of real numbers
bumby bumby (Apr 09 2021 at 15:41):
interesting i will try thanks
Last updated: May 14 2021 at 13:24 UTC