linear independent with a non-hardcoded list of vectors

Stream: new members

[David Chanin]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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]

Indeed, that's how docs#linear_independent_insert is stated

[Eric Wieser]

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]

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]

Thank you so much for the tips!

[Eric Wieser]

docs#linear_independent_fin_cons, docs#linear_independent.fin_cons'

[Eric Wieser]

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