rank_le_height

Mathlib.LinearAlgebra.Matrix.Rank

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

← MathLib Explorer

English

For A ∈ Matrix(Fintype m) × Matrix(Fintype n) over R, rank(A) ≤ m.

Русский

Для матрицы A над R размерности m×n (с m элементами в множестве Финит) ранг(A) ≤ m.

LaTeX

$$$\operatorname{rank}(A) \le m$$$

Lean4

theorem rank_le_height [Nontrivial R] {m n : ℕ} (A : Matrix (Fin m) (Fin n) R) : A.rank ≤ m :=
  A.rank_le_card_height.trans <| (Fintype.card_fin m).le

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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