of_basis — Mathlib

English

A free module with a basis indexed by a finite set is finite.

Русский

Свободный модуль с базисом, индексируемым конечным множеством, конечно по размеру.

LaTeX

$$$$ \exists \iota, \big( \mathrm{Finite}(\iota) \land \exists b: \mathrm{Basis}(\iota, R, M) \big) \;\Rightarrow\; \mathrm{Finite}(M). $$$$

Lean4

/-- A free module with a basis indexed by a `Fintype` is finite. -/
theorem of_basis {R M ι : Type*} [Semiring R] [AddCommMonoid M] [Module R M] [_root_.Finite ι] (b : Basis ι R M) :
    Module.Finite R M := by
  cases nonempty_fintype ι
  classical
  refine ⟨⟨Finset.univ.image b, ?_⟩⟩
  simp only [Set.image_univ, Finset.coe_univ, Finset.coe_image, Basis.span_eq]

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