mathlib documentation

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 #

TODO #

noncomputable def matrix.rank {m : Type u_1} {n : Type u_2} {K : Type u_4} [fintype n] [decidable_eq n] [field K] (A : matrix m 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 : matrix m 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 : matrix m n K) (B : matrix n 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 : matrix n 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 : matrix m n K) {M₁ : Type u_3} {M₂ : Type u_5} [add_comm_group M₁] [add_comm_group M₂] [module K M₁] [module K M₂] (v₁ : basis m K M₁) (v₂ : basis n 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 : matrix m 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