rank_le_card_height — Mathlib

English

For any matrix A with rows indexed by a finite set, the rank is at most the number of rows.

Русский

Для любой матрицы A, ранг не превосходит количества строк.

LaTeX

$$$\operatorname{rank}(A) \le |\text{rows}(A)|$$$

Lean4

theorem rank_le_card_height [Fintype m] [Nontrivial R] (A : Matrix m n R) : A.rank ≤ Fintype.card m :=
  by
  haveI : Module.Finite R (m → R) := Module.Finite.pi
  haveI : Module.Free R (m → R) := Module.Free.pi _ _
  exact (Submodule.finrank_le _).trans (finrank_pi R).le

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