# Rank of matrices #

The rank of a matrix A is defined to be the rank of range of the linear map corresponding to A. This definition does not depend on the choice of basis, see Matrix.rank_eq_finrank_range_toLin.

## Main declarations #

• Matrix.rank: the rank of a matrix

## TODO #

• Do a better job of generalizing over ℚ, ℝ, and ℂ in Matrix.rank_transpose and Matrix.rank_conjTranspose. See this Zulip thread.
noncomputable def Matrix.rank {m : Type u_2} {n : Type u_3} {R : Type u_5} [] [] (A : Matrix m n R) :

The rank of a matrix is the rank of its image.

Equations
Instances For
@[simp]
theorem Matrix.rank_one {n : Type u_3} {R : Type u_5} [] [] [] :
@[simp]
theorem Matrix.rank_zero {m : Type u_2} {n : Type u_3} {R : Type u_5} [] [] [] :
= 0
theorem Matrix.rank_le_card_width {m : Type u_2} {n : Type u_3} {R : Type u_5} [] [] (A : Matrix m n R) :
A.rank
theorem Matrix.rank_le_width {R : Type u_5} [] {m : } {n : } (A : Matrix (Fin m) (Fin n) R) :
A.rank n
theorem Matrix.rank_mul_le_left {m : Type u_2} {n : Type u_3} {o : Type u_4} {R : Type u_5} [] [] [] (A : Matrix m n R) (B : Matrix n o R) :
(A * B).rank A.rank
theorem Matrix.rank_mul_le_right {m : Type u_2} {n : Type u_3} {o : Type u_4} {R : Type u_5} [] [] [] (A : Matrix m n R) (B : Matrix n o R) :
(A * B).rank B.rank
theorem Matrix.rank_mul_le {m : Type u_2} {n : Type u_3} {o : Type u_4} {R : Type u_5} [] [] [] (A : Matrix m n R) (B : Matrix n o R) :
(A * B).rank min A.rank B.rank
theorem Matrix.rank_unit {n : Type u_3} {R : Type u_5} [] [] [] (A : (Matrix n n R)ˣ) :
(A).rank =
theorem Matrix.rank_of_isUnit {n : Type u_3} {R : Type u_5} [] [] [] (A : Matrix n n R) (h : ) :
A.rank =
@[simp]
theorem Matrix.rank_mul_eq_left_of_isUnit_det {m : Type u_2} {n : Type u_3} {R : Type u_5} [] [] [] (A : Matrix n n R) (B : Matrix m n R) (hA : IsUnit A.det) :
(B * A).rank = B.rank

Right multiplying by an invertible matrix does not change the rank

@[simp]
theorem Matrix.rank_mul_eq_right_of_isUnit_det {m : Type u_2} {n : Type u_3} {R : Type u_5} [] [] [] [] (A : Matrix m m R) (B : Matrix m n R) (hA : IsUnit A.det) :
(A * B).rank = B.rank

Left multiplying by an invertible matrix does not change the rank

theorem Matrix.rank_submatrix_le {m : Type u_2} {n : Type u_3} {R : Type u_5} [] [] [] (f : nm) (e : n m) (A : Matrix m m R) :
(A.submatrix f e).rank A.rank

Taking a subset of the rows and permuting the columns reduces the rank.

theorem Matrix.rank_reindex {m : Type u_2} {n : Type u_3} {R : Type u_5} [] [] [] (e₁ : m n) (e₂ : m n) (A : Matrix m m R) :
((Matrix.reindex e₁ e₂) A).rank = A.rank
@[simp]
theorem Matrix.rank_submatrix {m : Type u_2} {n : Type u_3} {R : Type u_5} [] [] [] (A : Matrix m m R) (e₁ : n m) (e₂ : n m) :
(A.submatrix e₁ e₂).rank = A.rank
theorem Matrix.rank_eq_finrank_range_toLin {m : Type u_2} {n : Type u_3} {R : Type u_5} [] [] [] [] {M₁ : Type u_6} {M₂ : Type u_7} [] [] [Module R M₁] [Module R M₂] (A : Matrix m n R) (v₁ : Basis m R M₁) (v₂ : Basis n R M₂) :
theorem Matrix.rank_le_card_height {m : Type u_2} {n : Type u_3} {R : Type u_5} [] [] [] (A : Matrix m n R) :
A.rank
theorem Matrix.rank_le_height {R : Type u_5} [] {m : } {n : } (A : Matrix (Fin m) (Fin n) R) :
A.rank m
theorem Matrix.rank_eq_finrank_span_cols {m : Type u_2} {n : Type u_3} {R : Type u_5} [] [] (A : Matrix m n R) :
A.rank = FiniteDimensional.finrank R (Submodule.span R (Set.range A.transpose))

The rank of a matrix is the rank of the space spanned by its columns.

theorem Matrix.rank_diagonal {m : Type u_2} {R : Type u_5} [] [] [] [] (w : mR) :
().rank = Fintype.card { i : m // w i 0 }

The rank of a diagnonal matrix is the count of non-zero elements on its main diagonal

### Lemmas about transpose and conjugate transpose #

This section contains lemmas about the rank of Matrix.transpose and Matrix.conjTranspose.

Unfortunately the proofs are essentially duplicated between the two; ℚ is a linearly-ordered ring but can't be a star-ordered ring, while ℂ is star-ordered (with open ComplexOrder) but not linearly ordered. For now we don't prove the transpose case for ℂ.

TODO: the lemmas Matrix.rank_transpose and Matrix.rank_conjTranspose current follow a short proof that is a simple consequence of Matrix.rank_transpose_mul_self and Matrix.rank_conjTranspose_mul_self. This proof pulls in unnecessary assumptions on R, and should be replaced with a proof that uses Gaussian reduction or argues via linear combinations.

theorem Matrix.ker_mulVecLin_conjTranspose_mul_self {m : Type u_2} {n : Type u_3} {R : Type u_5} [] [] [] [] [] [] (A : Matrix m n R) :
LinearMap.ker (A.conjTranspose * A).mulVecLin = LinearMap.ker A.mulVecLin
theorem Matrix.rank_conjTranspose_mul_self {m : Type u_2} {n : Type u_3} {R : Type u_5} [] [] [] [] [] [] (A : Matrix m n R) :
(A.conjTranspose * A).rank = A.rank
@[simp]
theorem Matrix.rank_conjTranspose {m : Type u_2} {n : Type u_3} {R : Type u_5} [] [] [] [] [] [] (A : Matrix m n R) :
A.conjTranspose.rank = A.rank

TODO: prove this in greater generality.

@[simp]
theorem Matrix.rank_self_mul_conjTranspose {m : Type u_2} {n : Type u_3} {R : Type u_5} [] [] [] [] [] [] (A : Matrix m n R) :
(A * A.conjTranspose).rank = A.rank
theorem Matrix.ker_mulVecLin_transpose_mul_self {m : Type u_2} {n : Type u_3} {R : Type u_5} [] [] (A : Matrix m n R) :
LinearMap.ker (A.transpose * A).mulVecLin = LinearMap.ker A.mulVecLin
theorem Matrix.rank_transpose_mul_self {m : Type u_2} {n : Type u_3} {R : Type u_5} [] [] (A : Matrix m n R) :
(A.transpose * A).rank = A.rank
@[simp]
theorem Matrix.rank_transpose {m : Type u_2} {n : Type u_3} {R : Type u_5} [] [] (A : Matrix m n R) :
A.transpose.rank = A.rank

TODO: prove this in greater generality.

@[simp]
theorem Matrix.rank_self_mul_transpose {m : Type u_2} {n : Type u_3} {R : Type u_5} [] [] (A : Matrix m n R) :
(A * A.transpose).rank = A.rank
theorem Matrix.rank_eq_finrank_span_row {m : Type u_2} {n : Type u_3} {R : Type u_5} [] [] (A : Matrix m n R) :
A.rank =

The rank of a matrix is the rank of the space spanned by its rows.

TODO: prove this in a generality that works for ℂ too, not just ℚ and ℝ.