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 : 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] :
1.rank = fintype.card n
@[simp]
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) :
A.rank ≤ fintype.card 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) :
theorem
matrix.rank_unit
{n : Type u_2}
{K : Type u_4}
[fintype n]
[decidable_eq n]
[field K]
(A : (matrix n n K)ˣ) :
↑A.rank = fintype.card n
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) :
A.rank = fintype.card n
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₂) :
A.rank = finite_dimensional.finrank K ↥(linear_map.range (⇑(matrix.to_lin v₂ v₁) A))
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) :
A.rank ≤ fintype.card m