finset_card_le_finrank — Mathlib

English

In the finite setting, a linear independent family indexed by a finite set has cardinal at most finrank M.

Русский

В конечной обстановке линейно независимая семейство с индексами в конечном множество имеет кардинал ≤ finrank M.

LaTeX

$$$[Module.Finite R M] {b : ι → M}, \text{LinearIndependent } R b \Rightarrow \#ι \le \operatorname{finrank} R M.$$$

Lean4

theorem finset_card_le_finrank [Module.Finite R M] {b : Finset M} (h : LinearIndependent R (fun x => x : b → M)) :
    b.card ≤ finrank R M := by
  rw [← Fintype.card_coe]
  exact h.fintype_card_le_finrank

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