fintype_card_le_finrank — Mathlib

English

For a finite module M, any LI family b : ι → M satisfies #ι ≤ finrank M.

Русский

Для конечного модуля M любая LI-последовательность удовлетворяет #ι ≤ finrank M.

LaTeX

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

Lean4

theorem fintype_card_le_finrank [Module.Finite R M] {ι : Type*} [Fintype ι] {b : ι → M} (h : LinearIndependent R b) :
    Fintype.card ι ≤ finrank R M := by simpa using h.cardinalMk_le_finrank

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