eRank_le_card_height — Mathlib

English

Under StrongRankCondition and finite m, eRank ≤ ENat.card m.

Русский

При условии StrongRankCondition и конечного m, eRank ≤ ENat.card m.

LaTeX

$$$A.eRank \le ENat.card\,m.$$$

Lean4

theorem eRank_le_card_height [StrongRankCondition R] (A : Matrix m n R) : A.eRank ≤ ENat.card m := by
  classical
  wlog hfin : Finite m
  · simp [ENat.card_eq_top.2 (by simpa using hfin)]
  have _ := Fintype.ofFinite m
  rw [ENat.card_eq_coe_fintype_card, eRank, toENat_le_nat]
  exact A.cRank_le_card_height

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