Finitely-generated Module - Formal Definition

Formal Definition

The left R-module M is finitely generated if and only if there exist a₁, a₂, ..., a_n in M such that for all x in M, there exist r₁, r₂, ..., r_n in R with x = r₁a₁ + r₂a₂ + ... + r_na_n.

The set {a₁, a₂, ..., a_n} is referred to as a generating set for M in this case.

In the case where the module M is a vector space over a field R, and the generating set is linearly independent, n is well-defined and is referred to as the dimension of M (well-defined means that any linearly independent generating set has n elements: this is the dimension theorem for vector spaces).