## Stream: PR reviews

### Topic: 4567 linear independent

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

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 (Oct 11 2020 at 02:38):

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

#### Yury G. Kudryashov (Oct 11 2020 at 02:56):

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

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