Linear Independence and Matrices

This file provides lemmas about linear independence in the context of matrices that are not present in Mathlib.

theorem Matrix.linearIndependent_iff_fromCols_zero {X : Type u_1} {Y : Type u_2} {R : Type u_3} [Ring R] (A : Matrix X Y R) (Y₀ : Type u_4) : LinearIndependent R A ↔ LinearIndependent R (A ◫ 0)

theorem linearIndepOn_matrix_elem_range_iff_subst {α : Type u_1} {X X' Y I : Set α} {R : Type} [Semiring R] {A : Matrix (↑X) (↑Y) R} {A' : Matrix (↑X') (↑Y) R} (hXX : X = X') (hIX : I ⊆ X) (hAA : A = ⋯ ▸ A') : let_fun hIX' := ⋯; LinearIndepOn R A hIX.elem.range ↔ LinearIndepOn R A' hIX'.elem.range

theorem linearIndepOn_matrix_inter_iff_subst {α : Type u_1} {X X' Y I : Set α} {R : Type} [Semiring R] {A : Matrix (↑X) (↑Y) R} {A' : Matrix (↑X') (↑Y) R} (hXX : X = X') (hAA : A = ⋯ ▸ A') : LinearIndepOn R A (Subtype.val ⁻¹' I) ↔ LinearIndepOn R A' (Subtype.val ⁻¹' I)

theorem Matrix.one_linearIndependent {α : Type u_1} {R : Type u_2} [DecidableEq α] [Ring R] : LinearIndependent R 1

The identity matrix has linearly independent rows.

theorem IsUnit.linearIndependent_matrix {α : Type u_1} {R : Type u_2} [DecidableEq α] [Fintype α] [Ring R] {A : Matrix α α R} (hA : IsUnit A) : LinearIndependent R A

Every invertible matrix has linearly independent rows (unapplied version).

theorem Matrix.not_linearIndependent_of_rank_lt {X : Type u_1} {Y : Type u_2} {F : Type u_3} [Fintype X] [Fintype Y] [Field F] (A : Matrix X Y F) (hA : A.rank < #X) : ¬LinearIndependent F A

theorem Matrix.not_linearIndependent_of_too_many_rows {X : Type u_1} {Y : Type u_2} {F : Type u_3} [Fintype X] [Fintype Y] [Field F] (A : Matrix X Y F) (hYX : #Y < #X) : ¬LinearIndependent F A

theorem Matrix.exists_submatrix_rank {X : Type u_1} {Y : Type u_2} {F : Type u_3} [Fintype X] [Fintype Y] [Field F] (A : Matrix X Y F) : ∃ (r : Fin A.rank → X), (A.submatrix r id).rank = A.rank

theorem Matrix.linearIndependent_iff_exists_submatrix_unit {X : Type u_1} {Y : Type u_2} {F : Type u_3} [Fintype X] [Fintype Y] [Field F] [DecidableEq X] (A : Matrix X Y F) : LinearIndependent F A ↔ ∃ (f : X → Y), IsUnit (A.submatrix id f)

Rows of a matrix are linearly independent iff the matrix contains a nonsigular square submatrix of full height.

theorem Matrix.linearIndependent_iff_exists_submatrix_det {X : Type u_1} {Y : Type u_2} {F : Type u_3} [Fintype X] [Fintype Y] [Field F] [DecidableEq X] (A : Matrix X Y F) : LinearIndependent F A ↔ ∃ (f : X → Y), (A.submatrix id f).det ≠ 0

Rows of a matrix are linearly independent iff the matrix contains a square submatrix of full height with nonzero det.