eRank_toNat_eq_finrank

Mathlib.LinearAlgebra.Matrix.Rank

URI: https://scilib.ai/kg/mathlib#Matrix.eRank_toNat_eq_finrank

English

As above, eRank.toNat equals finrank(span(range A.col)).

Русский

Как выше, 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

theorem eRank_toNat_eq_finrank (A : Matrix m n R) : A.eRank.toNat = Module.finrank R (span R (range A.col)) :=
  toNat_toENat ..

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru