Zulip Chat Archive

Stream: new members

Topic: vector spaces


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

view this post on Zulip 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 + and , how can I show this is a vector space?"

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

view this post on Zulip Eric Wieser (Apr 09 2021 at 14:36):

You'll probably end up wanting docs#vector_space (aka docs#module aka docs#semimodule), but I think it would be valuable for you to expand on your question

view this post on Zulip Anne Baanen (Apr 09 2021 at 14:37):

Or maybe docs#submodule since we're starting with a set.

view this post on Zulip bumby bumby (Apr 09 2021 at 15:05):

exactly

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

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

view this post on Zulip bumby bumby (Apr 09 2021 at 15:41):

interesting i will try thanks


Last updated: May 14 2021 at 13:24 UTC