rank_eq_finrank_span_cols — Mathlib

English

The natural part of cRank equals the usual rank: cRank(A).toNat = rank(A).

Русский

Единичная часть cRank совпадает с обычным рангом: cRank(A).toNat = rank(A).

LaTeX

$$$cRank(A).toNat = \operatorname{rank}(A)$$$

Lean4

/-- The rank of a matrix is the rank of the space spanned by its columns. -/
theorem rank_eq_finrank_span_cols (A : Matrix m n R) : A.rank = finrank R (Submodule.span R (Set.range A.col)) := by
  rw [rank, Matrix.range_mulVecLin]

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