# Zulip Chat Archive

## 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:16):

docs#linear_independent_fin_cons, docs#linear_independent.fin_cons'

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