rank — Mathlib

English

The rank of A equals the dimension of the image of the associated linear map, i.e., rank(A) = dim_R(range(A.mulVecLin)).

Русский

Ранг A равен размерности образа соответствующего линейного отображения: rank(A) = dim_R(range(A.mulVecLin)).

LaTeX

$$$\operatorname{rank}(A) = \dim_R(\operatorname{range}(A\!:\!\mathrm{mulVecLin})).$$$

Lean4

/-- The rank of a matrix is the rank of its image. -/
noncomputable def rank (A : Matrix m n R) : ℕ :=
  finrank R <| LinearMap.range A.mulVecLin

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