rank_transpose — Mathlib

English

The rank of the transpose A^T equals the rank of A.

Русский

Ранк транспонирования A^T равен рангу A.

LaTeX

$$$ \operatorname{rank}(A^{T}) = \operatorname{rank}(A). $$$

Lean4

@[simp]
theorem rank_transpose [Field R] [Fintype m] (A : Matrix m n R) : Aᵀ.rank = A.rank := by
  classical
    rw [Aᵀ.rank_eq_finrank_range_toLin (Pi.basisFun R n).dualBasis (Pi.basisFun R m).dualBasis, toLin_transpose, ←
    LinearMap.dualMap_def, LinearMap.finrank_range_dualMap_eq_finrank_range, toLin_eq_toLin', toLin'_apply', rank]

Похожие утверждения