cardinal_le_rank — Mathlib

English

For a linearly independent family v: ι → M, the index cardinality satisfies #ι ≤ rank_R(M).

Русский

Для линейно независимой семейства v: ι → M кардинал множества индексов удовлетворяет #ι ≤ rank_R(M).

LaTeX

$$$\#\iota \le \operatorname{rank}_R(M)$$$

Lean4

theorem cardinal_le_rank {ι : Type v} {v : ι → M} (hv : LinearIndependent R v) : #ι ≤ Module.rank R M := by
  simpa using hv.cardinal_lift_le_rank

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