cRank_le_card_height — Mathlib

English

Over a StrongRankCondition ring R and with finite m, the rank of A is at most the cardinality of m.

Русский

При условии StrongRankCondition для кольца R и конечного множества индексов m, cRank(A) ≤ card m.

LaTeX

$$$A.cRank \le |m|$, under the assumptions.$$

Lean4

theorem cRank_le_card_height [StrongRankCondition R] [Fintype m] (A : Matrix m n R) : A.cRank ≤ Fintype.card m :=
  (Submodule.rank_le (span R (range Aᵀ))).trans <| by rw [rank_fun']

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