Linear independence of rows in partitioned matrices

This file proves that the rows of a column-partitioned matrix [A | B] are linearly independent as soon as the rows of one of its blocks are: two distinct combinations of the rows already differ on the columns of that block, so no nontrivial combination of the rows vanishes.

The main instance is a block that is an identity matrix, whose rows are linearly independent by Matrix.linearIndependent_row_one. Consequently a matrix in systematic form has full row rank, which is what turns a row count into a dimension: over a field, [I | A] has as many rows as the dimension of the code it generates, and [B | I] has as many rows as the codimension of the code it checks.

Main declarations

• Matrix.linearIndependent_row_fromCols_of_left, Matrix.linearIndependent_row_fromCols_of_right: the rows of [A | B] are linearly independent when those of A, respectively B, are.
• Matrix.linearIndependent_row_one_fromCols: the rows of [I | A] are linearly independent.
• Matrix.linearIndependent_row_fromCols_one: the rows of [B | I] are linearly independent.

theorem Matrix.linearIndependent_row_fromCols_of_left {R : Type u_1} {m : Type u_2} {n₁ : Type u_3} {n₂ : Type u_4} [Semiring R] {A : Matrix m n₁ R} (hA : LinearIndependent R A.row) (B : Matrix m n₂ R) : LinearIndependent R (A.fromCols B).row

If the rows of the left block A are linearly independent, so are the rows of [A | B].

theorem Matrix.linearIndependent_row_fromCols_of_right {R : Type u_1} {m : Type u_2} {n₁ : Type u_3} {n₂ : Type u_4} [Semiring R] {B : Matrix m n₂ R} (hB : LinearIndependent R B.row) (A : Matrix m n₁ R) : LinearIndependent R (A.fromCols B).row

If the rows of the right block B are linearly independent, so are the rows of [A | B].

theorem Matrix.linearIndependent_row_one_fromCols {R : Type u_1} {m : Type u_2} {n₂ : Type u_4} [Semiring R] [DecidableEq m] (A : Matrix m n₂ R) : LinearIndependent R (fromCols 1 A).row

The rows of a systematic matrix [I | A] are linearly independent.

theorem Matrix.linearIndependent_row_fromCols_one {R : Type u_1} {m : Type u_2} {n₁ : Type u_3} [Semiring R] [DecidableEq m] (B : Matrix m n₁ R) : LinearIndependent R (B.fromCols 1).row

The rows of a systematic matrix [B | I] are linearly independent.