Module.Finite.of_basis

theorem Module.Finite.of_basis : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : Finite ι], Basis ι R M → Module.Finite R M

This theorem states that a free module with a basis indexed by a `Fintype` (finite type) is finite. More formally, for any given Semiring `R`, Additive Commutative Monoid `M`, and any type `ι` that is finite, if there exists a basis indexed by `ι` for the module `M` over the ring `R`, then the module `M` over the ring `R` is finite. This theorem is fundamental in the theory of modules over rings, especially in the context of finite dimensional vector spaces.

More concisely: A free module over a ring with a finite basis is finite.