rank_lt_aleph0_iff — Mathlib

English

Let M be a free module over R. The rank of M is finite if and only if M is a finite R-module.

Русский

Пусть M — свободный модуль над R. Ранг M конечен тогда и только тогда, когда M является конечным модулем над R.

LaTeX

$$$$ Module\\;rank\\,R\\,M < \\aleph_0 \\;\\leftrightarrow\\; Module.Finite\\,R\\,M $$$$

Lean4

/-- See `rank_lt_aleph0` for the inverse direction without `Module.Free R M`. -/
theorem rank_lt_aleph0_iff : Module.rank R M < ℵ₀ ↔ Module.Finite R M :=
  by
  rw [Free.rank_eq_card_chooseBasisIndex, mk_lt_aleph0_iff]
  exact ⟨fun h ↦ Finite.of_basis (Free.chooseBasis R M), fun I ↦ Finite.of_fintype (Free.ChooseBasisIndex R M)⟩

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