4567 linear independent

Stream: PR reviews

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Kevin Buzzard]

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