data.matrix.rank

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_to_lin.

Main declarations #

• matrix.rank: the rank of a matrix

TODO #

• Show that matrix.rank is equal to the row-rank and column-rank
• Generalize away from fields
noncomputable def matrix.rank {m : Type u_1} {n : Type u_2} {K : Type u_4} [fintype n] [decidable_eq n] [field K] (A : n K) :

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

Equations
@[simp]
theorem matrix.rank_one {n : Type u_2} {K : Type u_4} [fintype n] [decidable_eq n] [field K] :
@[simp]
theorem matrix.rank_zero {n : Type u_2} {K : Type u_4} [fintype n] [decidable_eq n] [field K] :
0.rank = 0
theorem matrix.rank_le_card_width {m : Type u_1} {n : Type u_2} {K : Type u_4} [fintype n] [decidable_eq n] [field K] (A : n K) :
theorem matrix.rank_le_width {K : Type u_4} [field K] {m n : } (A : matrix (fin m) (fin n) K) :
A.rank n
theorem matrix.rank_mul_le {m : Type u_1} {n : Type u_2} {o : Type u_3} {K : Type u_4} [fintype n] [fintype o] [decidable_eq n] [decidable_eq o] [field K] (A : n K) (B : o K) :
(A.mul B).rank A.rank
theorem matrix.rank_unit {n : Type u_2} {K : Type u_4} [fintype n] [decidable_eq n] [field K] (A : (matrix n n K)ˣ) :
theorem matrix.rank_of_is_unit {n : Type u_2} {K : Type u_4} [fintype n] [decidable_eq n] [field K] (A : n K) (h : is_unit A) :
theorem matrix.rank_eq_finrank_range_to_lin {m : Type u_1} {n : Type u_2} {K : Type u_4} [m_fin : fintype m] [fintype n] [decidable_eq n] [field K] (A : n K) {M₁ : Type u_3} {M₂ : Type u_5} [add_comm_group M₁] [add_comm_group M₂] [ M₁] [ M₂] (v₁ : K M₁) (v₂ : K M₂) :
theorem matrix.rank_le_card_height {m : Type u_1} {n : Type u_2} {K : Type u_4} [m_fin : fintype m] [fintype n] [decidable_eq n] [field K] (A : n K) :
theorem matrix.rank_le_height {K : Type u_4} [field K] {m n : } (A : matrix (fin m) (fin n) K) :
A.rank m