cRank — Mathlib

English

The rank of a matrix A is defined as the dimension, over R, of the column space, i.e., of span_R(range Aᵀ). It is a cardinal number.

Русский

Ранк матрицы A определяется как размерность пространства столбцов: размерность подпространства span_R(range(Aᵀ)) над R.

LaTeX

$$$\operatorname{cRank}(A) = \operatorname{rank}_R\big( \operatorname{span}_R(\operatorname{range}(A^T))\big).$$$

Lean4

/-- The rank of a matrix, defined as the dimension of its column space, as a cardinal. -/
noncomputable def cRank (A : Matrix m n R) : Cardinal :=
  Module.rank R <| span R <| range Aᵀ

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