Zulip Chat Archive

Stream: PR reviews

Topic: 4567 linear independent


view this post on Zulip Yury G. Kudryashov (Oct 11 2020 at 02:37):

In #4567 I refactored linear_algebra/linear_independent to provide more lemmas about type-level operations (sum, option) instead of concentrating on families indexed by sets. Results about families indexed by sets follow from equivalences with type operations.
Among other theorems, it adds

lemma linear_independent_pair {x y : V} (hx : x  0) (hy :  a : K, a  x  y) :
  linear_independent K (coe : ({x, y} : set V)  V) := sorry

lemma linear_independent_fin_cons {n} {v : fin n  V} :
  linear_independent K (fin.cons x v : fin (n + 1)  V) 
    linear_independent K v  x  submodule.span K (range v) := sorry

lemma linear_independent.fin_cons {n} {v : fin n  V} (hv : linear_independent K v)
  (hx : x  submodule.span K (range v)) :
  linear_independent K (fin.cons x v : fin (n + 1)  V) :=
linear_independent_fin_cons.2 hv, hx

lemma linear_independent_fin_succ {n} {v : fin (n + 1)  V} :
  linear_independent K v 
    linear_independent K (fin.tail v)  v 0  submodule.span K (range $ fin.tail v) :=
sorry

lemma linear_independent_fin2 {f : fin 2  V} :
  linear_independent K f  f 1  0   a : K, a  f 1  f 0 :=
sorry

view this post on Zulip Yury G. Kudryashov (Oct 11 2020 at 02:38):

These lemmas should make proving linear independence of ![v₁, v₂, v₃] less painful.

view this post on Zulip Yury G. Kudryashov (Oct 11 2020 at 02:56):

What do you think about a PR review sprint? We have 41 PRs awaiting review.

view this post on Zulip Kevin Buzzard (Oct 11 2020 at 07:30):

Give me a few days and I'll sprint :D


Last updated: May 09 2021 at 12:14 UTC