eRank — Mathlib

English

The natural value of eRank equals the finite rank of the column span, i.e., eRank.toNat = finrank(span(range A.col)).

Русский

Естественная величина eRank равна конечной размерности пространства столбцов: eRank.toNat = finrank(span(range A.col)).

LaTeX

$$$A.eRank.toNat = \operatorname{finrank}_R\big(\operatorname{span}_R(\operatorname{range}(A^{\text{col}}))\big).$$$

Lean4

/-- The rank of a matrix, defined as the dimension of its column space, as a term in `ℕ∞`. -/
noncomputable def eRank (A : Matrix m n R) : ℕ∞ :=
  A.cRank.toENat

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