finite_of_rank_eq_nat — Mathlib

English

If M is a free module of rank n (finite), then M is finite as a module.

Русский

Если M свободный модуль ранга n (конечного), то M конечно в смысле как модуль.

LaTeX

$$$[\text{Module.Free } R M] \Rightarrow (\operatorname{rank}_R M = n \Rightarrow \text{Module.Finite } R M).$$$

Lean4

theorem finite_of_rank_eq_nat [Module.Free R M] {n : ℕ} (h : Module.rank R M = n) : Module.Finite R M :=
  by
  nontriviality R
  obtain ⟨⟨ι, b⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
  have := mk_lt_aleph0_iff.mp <| b.linearIndependent.cardinal_le_rank |>.trans_eq h |>.trans_lt <| nat_lt_aleph0 n
  exact Module.Finite.of_basis b

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