rank_le_card_width — Mathlib

English

For a finite-type matrix A of size m×n over a commutative ring R, the rank of A is at most the number of columns, i.e., rank(A) ≤ card n.

Русский

Для матрицы размером m×n над коммутативным кольцом R ранг матрицы не превосходит числа столбцов: rank(A) ≤ card n.

LaTeX

$$$$ \\operatorname{rank}(A) \\le \\#n $$$$

Lean4

theorem rank_le_card_width [Nontrivial R] (A : Matrix m n R) : A.rank ≤ Fintype.card n :=
  by
  haveI : Module.Finite R (n → R) := Module.Finite.pi
  haveI : Module.Free R (n → R) := Module.Free.pi _ _
  exact A.mulVecLin.finrank_range_le.trans_eq (finrank_pi _)

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