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 Y R : Type} [Ring R] (A : Matrix X Y R) (Y₀ : Type) : LinearIndependent R A ↔ LinearIndependent R (A ◫ 0)

theorem IsUnit.linearIndependent_matrix {α R : Type} [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 Y F : Type} [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 Y F : Type} [Fintype X] [Fintype Y] [Field F] (A : Matrix X Y F) (hYX : #Y < #X) : ¬LinearIndependent F A

theorem Matrix.exists_submatrix_rank {X Y F : Type} [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 Y F : Type} [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 Y F : Type} [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.