cardinalMk_le_finrank — Mathlib

English

If b is a linearly independent family with index set ι, then the cardinal of ι is at most finrank M.

Русский

Если b — линейно независимая семья с индексом ι, то |ι| ≤ finrank M.

LaTeX

$$$\#ι \le \operatorname{finrank} R M,$$$

Lean4

theorem cardinalMk_le_finrank [Module.Finite R M] {ι : Type w} {b : ι → M} (h : LinearIndependent R b) :
    #ι ≤ finrank R M := by
  rw [← lift_le.{max v w}]
  simpa only [← finrank_eq_rank, lift_natCast, lift_le_nat_iff] using h.cardinal_lift_le_rank

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