## 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 + and •, 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):

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

#### Anne Baanen (Apr 09 2021 at 14:37):

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

exactly

#### 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

#### Esteban Estupinan (Jul 27 2021 at 20:40):

hi zulip members, I comment you I m trying prove that the intersection of subspaces of a vector space is another subspace. I was reading some of indexed families in logic and proof book to write the collection of subspaces in lean. I think it is right in my code. I have a little idea to prove. The problem is that I dont know how introduce W as the intersection of the subspaces. I think this should be written in the "carrier" part of the code. I would appreciate a lot if you can help me in this part, I give you my code

#### Esteban Estupinan (Jul 27 2021 at 20:40):

import linear_algebra.basic

variables {R V I : Type*}

theorem t14 [field R] [add_comm_group V] [module R V]
{C: I → submodule R V} : submodule R V :=
{ carrier   := {},
zero_mem' :=
begin

end,
begin

end,
smul_mem' :=
begin

end, }


#### Alex J. Best (Jul 27 2021 at 20:49):

Sure, as you say the carrier should be the intersection of the carriers of the submodules in C, if we write that lean will insert the right coercion from the submodules to sets for us:

import linear_algebra.basic

variables {R V I : Type*}

theorem t14 [field R] [add_comm_group V] [module R V]
{C: I → submodule R V} : submodule R V :=
{ carrier   := ⋂ i, C i,
zero_mem' :=
begin

end,
begin

end,
smul_mem' :=
begin

end, }


#### Alex J. Best (Jul 27 2021 at 20:51):

This should really be a def rather than a theorem I guess, as you are reallly defining the intersection of submodules as a submodule here.

#### Kevin Buzzard (Jul 27 2021 at 21:06):

I think that the morally correct and least confusing way to formalise such a question would be using unbundled subspaces. One could define is_subspace (S : set V) to be the predicate that S is (the underlying subset of) a subspace and then use set lemmas to prove the result. This is not how these things are handled in Lean but it seems to be easier to understand than our approach.

#### Esteban Estupinan (Jul 27 2021 at 23:49):

ok, after intro some hypothesis, I don't know if it's correct but I wanted using the simp only tactic maybe to simplify the general intersections and using rw tactic better, It is posible use simp only tactic with some Inter theorem ? if is not what would be another alternative?

#### Esteban Estupinan (Jul 27 2021 at 23:49):

import linear_algebra.basic

variables {R V I : Type*}

theorem t14 [field R] [add_comm_group V] [module R V]
{C: I → submodule R V} : submodule R V :=
{ carrier   := ⋂ i, C i,
zero_mem' :=
begin
simp only [] at ⊢,
rw
end,
begin
intros x y hx hy,
simp only [] at hx hy ⊢,
rw
end,
smul_mem' :=
begin
intros c x hx,
simp only [] at hx ⊢,
rw
end, }


#### Eric Wieser (Jul 28 2021 at 09:05):

Does simp only do anything at all here? simp is far more likely to be helpful

#### Esteban Estupinan (Jul 30 2021 at 14:55):

hi how are you, i'm trying to prove the following 3 theorems related to subspaces. first I started entering the hypothesis and thesis here I notice that there is a common error, especially when entering the "if and only if". Please if someone can help me to see what is wrong and how I can correct it this first part, thank you very much

imagen.png

#### Eric Wieser (Jul 30 2021 at 14:57):

What exactly do you mean? We can't help you with an error if you don't show the error.

now the codes

#### Esteban Estupinan (Jul 30 2021 at 14:58):

import linear_algebra.basic

variables {R V W : Type*}

theorem e18 [field R] [add_comm_group V] [module R V]
{x y : W} {a : R} (W ≠ ∅) : submodule R V ↔ (a * x ∈ W) ∧ (x + y ∈ W)
{ carrier   := W ⊆ V,
zero_mem' :=
begin

end,
begin

end,
smul_mem' :=
begin

end, }


#### Eric Wieser (Jul 30 2021 at 14:58):

(ah - you might not be aware there's a "press enter to send" checkbox at the bottom right that lets you put multiple lines in a single message)

ok a wil try

#### Eric Wieser (Jul 30 2021 at 14:59):

If you're doing 18, why do you have W ≠ ∅ which is an assumption from 17?

#### Patrick Massot (Jul 30 2021 at 15:00):

You messed up the quantifiers

#### Patrick Massot (Jul 30 2021 at 15:01):

But the text you are following is pretty sloppy with quantifiers, so this is not too suprising.

#### Esteban Estupinan (Jul 30 2021 at 15:03):

the code is of 17 and here is w is empty

#### Eric Wieser (Jul 30 2021 at 15:03):

Why did you call it e18 if it's for 17?

#### Esteban Estupinan (Jul 30 2021 at 15:04):

ups is error because in vsc I have with 17 sorry

#### Eric Wieser (Jul 30 2021 at 15:05):

• Hypotheses needs names. It should be (hW : W ≠ ∅)  not (W ≠ ∅)
• The format should be statement := proof not statement proof- you're missing the :=

#### Patrick Massot (Jul 30 2021 at 15:05):

I think the math errors are much more serious here.

#### Eric Wieser (Jul 30 2021 at 15:06):

I agree the math errors are also bad, but there's no hope of getting the binders right if you don't even know the syntax for binders well enough.

#### Eric Wieser (Jul 30 2021 at 15:12):

Part of your trouble here is that submodule is not used in the same way as "is a submodule". A rough translation of "is a submodule" is:

/-- The set W is a submodule of V if there exists a submodule W' whose elements are equal to
W. -/
abbreviation is_submodule (W : set V) : Prop := ∃ W' : submodule R V, W = ↑W'


#### Esteban Estupinan (Jul 30 2021 at 15:34):

the part of carrier until the end is correct?

#### Eric Wieser (Jul 30 2021 at 15:38):

Until you have the statement written down, that question isn't even meaningful - right now it's nonsense. You should start off by writing

lemma e17 (your assumptions) : your_statement := sorry


Only once lean accepts that you should you try to replace the sorry with a proof.

ok I will try

#### Esteban Estupinan (Jul 30 2021 at 16:26):

amm i tried it but I keep getting errors

import linear_algebra.basic

variables {R V W : Type*}

lemma e17 [field R] [add_comm_group V] [module R V]
(W set : V) : ∃ W' : submodule R V, W = ↑W' ↔ W ≠ ∅ := sorry


#### Eric Wieser (Jul 30 2021 at 16:31):

(W set : V) means "let W be a V and let setbe a V"

#### Patrick Massot (Jul 30 2021 at 16:32):

Esteban, I think you need to work much more on the basic syntax of Lean before trying to prove anything in linear algebra. Did you try any of the learning resources listed on https://leanprover-community.github.io/learn.html?

#### Patrick Massot (Jul 30 2021 at 16:33):

Otherwise you'll only gain frustration.

#### Esteban Estupinan (Jul 30 2021 at 16:36):

i trying proof set theory and with help few linear algebra

#### Esteban Estupinan (Jul 30 2021 at 16:49):

Lean has helped me to be more precise in the mathematical demonstrations like today that in the book they do not mention quantifiers or Eric Wieser's explanation of the sub-modules, thanks. I have a confusion, for each github project it is advisable to create an independent project in lean, right?

#### Eric Wieser (Jul 30 2021 at 17:07):

I think you're running into trouble because you're having to learn the lean syntax and the mathlib linear algebra library and what it means to state theorems precisely all at once. I agree with Patrick, you would do well to try out one of the many lean tutorial / exercise projects rather than picking your own problems to formalize.

#### Esteban Estupinan (Dec 28 2021 at 12:36):

Could you please tell me if the following reasoning is correct? To understand the theorem 1.9 red underline, I supposed start reasoning from the thesis of the theorem 1.5 ( stating that span (beta) contains span (S) = V) like "apply" tactic in lean, so to prove this thesis I need to prove the hipothesis, that I think is "show that S is subset of span(beta)", is correct this backward reasonning? thank you for your answers imagen.png imagen.png

#### Eric Wieser (Dec 28 2021 at 12:52):

Have you managed to state theorem 1.9 in lean?

#### Esteban Estupinan (Dec 28 2021 at 13:03):

not yet though i wish i could. First I wanted to see if my reasoning was correct and maybe then pass it on Lean

#### Martin Dvořák (Dec 28 2021 at 14:26):

The informal proof seems correct to me. Just be careful that β in Theorem 1.9 corresponds to S in Theorem 1.5

#### Martin Dvořák (Dec 28 2021 at 14:30):

IMO, the part that is underlined in red will be easy to formalize. I am more worried about not knowing how to formalize the local definition of β.

Last updated: Dec 20 2023 at 11:08 UTC