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