## Stream: new members

### Topic: linear independent with a non-hardcoded list of vectors

#### David Chanin (Jul 25 2022 at 10:38):

I understand I can say linear_independent ℝ ![![1,2,3], ![4,5,6]] when I have a hardcoded matrix like this, but I can't figure out how to say a list of vectors of length m are linearly independent. I'm trying to prove the following:

If v1,v2,...,vm is linearly independent in V, then 5v1-4v2, v2,...,vm then is also linearly independent.

I tried using a set with insert as follows, but linear_independent seems like it needs a matrix and not a set of vectors.

example
(k : Type)
(V : Type)
[field k] [add_comm_group V] [module k V]
(v1 v2 : V)
(remainingV: set V)
:
linear_independent k (insert v1 (insert v2 remainingV)) → linear_independent k (insert (5 • v1 - 4
• v2) (insert v2 remainingV))
:= begin
sorry
end


Is there a way to specify a matrix that's a set of vectors of length m without hardcoding specific vectors into a matrix?

#### Eric Wieser (Jul 25 2022 at 11:38):

Perhaps what you're missing is that ![a, b, c] is notation for matrix.vec_cons a ![b, c]

#### Eric Wieser (Jul 25 2022 at 11:38):

insert is used for {a, b, c} notation

#### Eric Wieser (Jul 25 2022 at 11:39):

However, there's another way out here; while with ![a, b, c] you're using fin 3 as the index type, you can work with {a, b, c} if you use coe_sort {a, b, c} as the index type and coe as the function!

#### Eric Wieser (Jul 25 2022 at 11:40):

Indeed, that's how docs#linear_independent_insert is stated

#### Eric Wieser (Jul 25 2022 at 11:41):

David Chanin said:

I tried using a set with insert as follows, but linear_independent seems like it needs a matrix and not a set of vectors.

Strictly speaking, ![![1,2,3], ![4,5,6]] is a tuple of tuples (or vector of vectors); a matrix would be !![1,2,3; 4,5,6].

#### David Chanin (Jul 25 2022 at 19:45):

aah ok, I think I understand what you mean (at least with vec_cons). I can write the following and it doesn't error! Now just need to figure how to actually prove it...

open matrix

example
(k : Type)
(V : Type)
(m : ℕ)
[field k] [add_comm_group V] [module k V]
(v1 v2 : V)
(baseV: fin m → V)
:
linear_independent k (vec_cons v1 (vec_cons v2 baseV)) → linear_independent k (vec_cons (5 • v1 - 4
• v2) (vec_cons v2 baseV))
:= begin ... end


#### David Chanin (Jul 25 2022 at 19:56):

Thank you so much for the tips!

#### Eric Wieser (Jul 25 2022 at 20:17):

matrix.vec_cons is defined as equal to docs#fin.cons, because the latter often elaborates badly due to dependent types

Last updated: Dec 20 2023 at 11:08 UTC