cRank_toNat_eq_rank

Mathlib.LinearAlgebra.Matrix.Rank

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

English

Same as the previous: cRank_toNat_eq_rank.

Русский

То же самое: cRank_toNat_eq_rank.

LaTeX

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

Lean4

@[simp]
theorem cRank_toNat_eq_rank (A : Matrix m n R) : A.cRank.toNat = A.rank := by
  rw [cRank_toNat_eq_finrank, ← rank_eq_finrank_span_cols]

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

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

Разделы

Аффилиация

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