linear-algebra-done-right

Stream: new members

[Vasily Ilin]

I am trying to formalize the following linear algebra exercise. I am running into needing to convert from set, which I know is finite, to finset. Is there a better way to set up the example to avoid this issue?

image.png

import tactic
import linear_algebra.basis
import data.real.basic
import data.complex.basic
import data.complex.module
import data.matrix.notation

variables (k : Type) (V : Type) [field k] [add_comm_group V] [module k V]

example (m : ℕ) (v : fin m → V) (lin_indep : linear_independent k v) (w : V) (not_lin_indep : ¬ linear_independent k (matrix.vec_cons w v)) : w ∈ submodule.span k (set.range v) :=
begin
  rw fintype.not_linear_independent_iff at not_lin_indep,
  cases not_lin_indep with g hg,
  simp only [pi.add_apply, smul_add, ne.def, finset.sum_add_distrib, ← finset.sum_smul] at hg,
  have : g 0 ≠ 0,
    sorry,
  rw mem_span_finset, -- does not work
  sorry,
end

[Yakov Pechersky]

I would say that part of the formalization is knowing that just because the problem statement is using an indexed collection over m vars doesn't mean you should

[Yakov Pechersky]

I also think your statement doesn't match the problem, you're using vec_cons when the statement is about ((+) w o v)

[Yakov Pechersky]

Maybe I'm mistaken that the two are different

[Yakov Pechersky]

You can noncomputably produce a finset from a set you know is finite, if "hs : set.finite s" then "hs.to_finset" is the finset that corresponds to s. You're using the construction "set.finite.to_finset"

[Yakov Pechersky]

You can also use docs#finset.image to produce a finset directly corresponding to the range of v

[Yakov Pechersky]

I don't remember what the shorthand for of finset.univ.image v would be

[Vasily Ilin]

You are right, I misread what the problem is actually asking...
Thank you for pointing it out and the hints

[Kyle Miller]

One of the easiest ways to (computably) get finsets from sets is docs#set.to_finset after importing data.set.finite

example {V : Type*} [decidable_eq V] (m : ℕ) (v : fin m → V) : finset V :=
set.to_finset (set.range v)

[Kyle Miller]

That module has fintype instances that wrap up all the underlying finset operations for you.