English
If a module has finite rank, then any basis indexed by ι with rank less than aleph0 has a nonempty fintype index.
Русский
Если ранг модуля конечен, то любой базис с индексацией ι и ранга < ℵ0 имеет непустой конечный индекс.
LaTeX
$$$[\text{Module.Rank } R M] < \aleph_0 \Rightarrow \text{Nonempty } (\text{Fintype } ι).$$$
Lean4
/-- If a module has a finite dimension, all bases are indexed by a finite type. -/
theorem nonempty_fintype_index_of_rank_lt_aleph0 {ι : Type*} (b : Basis ι R M) (h : Module.rank R M < ℵ₀) :
Nonempty (Fintype ι) := by
rwa [← Cardinal.lift_lt, ← b.mk_eq_rank, Cardinal.lift_aleph0, Cardinal.lift_lt_aleph0,
Cardinal.lt_aleph0_iff_fintype] at h