rank_le_width — Mathlib

English

Let R be a commutative ring. For every m,n ∈ ℕ and every A ∈ M_{m×n}(R), the rank of A does not exceed n.

Русский

Пусть R — коммутативное кольцо. Для любых m,n ∈ ℕ и любой A ∈ M_{m×n}(R) ранг A не превосходит n.

LaTeX

$$$\forall R [CommRing(R)], \forall m,n \in \mathbb{N}, \forall A \in M_{m\times n}(R): \operatorname{rank}(A) \le n$$$

Lean4

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

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