Matrix rank

This file records general results relating matrix rank to the corresponding linear maps.

Main results

• Matrix.rank_eq_card_iff_vecMul_injective characterizes full row rank by injectivity of right multiplication by the matrix.
• Matrix.rank_add_rank_le_rank_mul_add_card: Sylvester's rank inequality rank A + rank B ≤ rank (A * B) + n for an m × n matrix A and an n × o matrix B.

theorem Matrix.rank_eq_card_iff_vecMul_injective {K : Type u_1} [Field K] {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] (B : Matrix m n K) : B.rank = Fintype.card m ↔ Function.Injective fun (v : m → K) => vecMul v B

A matrix has full row rank exactly when right multiplication by it is injective.

theorem Matrix.rank_add_rank_le_rank_mul_add_card {K : Type u_1} [Field K] {m : Type u_2} {n : Type u_3} [Fintype n] {o : Type u_4} [Fintype o] (A : Matrix m n K) (B : Matrix n o K) : A.rank + B.rank ≤ (A * B).rank + Fintype.card n

Sylvester's rank inequality: for an m × n matrix A and an n × o matrix B over a field, rank A + rank B ≤ rank (A * B) + n. Equivalently, multiplying by A lowers the rank of B by at most the nullity of A.