eRank_toNat_eq_rank

Mathlib.LinearAlgebra.Matrix.Rank

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

English

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

Русский

Единичная часть eRank равна рангу: eRank(A).toNat = rank(A).

LaTeX

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

Lean4

@[simp]
theorem eRank_toNat_eq_rank (A : Matrix m n R) : A.eRank.toNat = A.rank := by
  rw [eRank_toNat_eq_finrank, ← rank_eq_finrank_span_cols]

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

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

Разделы

Аффилиация

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