finrank_le_of_span_eq_top — Mathlib

English

If a family indexed by a finite set spans the whole module, then the module’s finrank is at most the size of the indexing index set.

Русский

Если семейство элементов, индексируемое конечным множеством, порождает весь модуль, то финразмерность модуля не превосходит размер множества индексирования.

LaTeX

$$$\operatorname{span}_R(\operatorname{range} v) = \top \Rightarrow \operatorname{finrank}_R(M) \le |\iota|$$$

Lean4

theorem finrank_le_of_span_eq_top {ι : Type*} [Fintype ι] {v : ι → M} (hv : Submodule.span R (Set.range v) = ⊤) :
    finrank R M ≤ Fintype.card ι := by
  classical
  rw [← finrank_top, ← hv]
  exact (finrank_span_le_card _).trans (by convert Fintype.card_range_le v; rw [Set.toFinset_card])

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