Deleting a row of a matrix

For a matrix G with rows indexed by ρ and a row index r, the matrix Matrix.deleteRow G r has rows indexed by {s : ρ // s ≠ r} and retains every row of G except row r. It is the submatrix of G along the inclusion of the remaining row indices.

Row deletion is used to remove a redundant row, one lying in the span of the other rows, while studying the row span of a matrix; for example, a generator matrix of a linear code can be pruned this way to a matrix with linearly independent rows that presents the same code.

Main definitions

• Matrix.deleteRow deletes one row of a matrix.

def Matrix.deleteRow {ι : Type u_1} {ρ : Type u_2} {R : Type u_3} (G : Matrix ρ ι R) (r : ρ) : Matrix { s : ρ // s ≠ r } ι R

The matrix obtained from G by deleting the row indexed by r.

Equations

• G.deleteRow r = G.submatrix Subtype.val id

@[simp]

theorem Matrix.deleteRow_apply {ι : Type u_1} {ρ : Type u_2} {R : Type u_3} (G : Matrix ρ ι R) (r : ρ) (s : { s : ρ // s ≠ r }) (i : ι) : G.deleteRow r s i = G (↑s) i

Evaluation of a matrix after deleting a row.

@[simp]

theorem Matrix.row_deleteRow {ι : Type u_1} {ρ : Type u_2} {R : Type u_3} (G : Matrix ρ ι R) (r : ρ) (s : { s : ρ // s ≠ r }) : (G.deleteRow r).row s = G.row ↑s

A retained row of deleteRow G r is the corresponding row of G.