Finitely Generated Vector Space has Finite Basis

Theorem

Let $K$ be a division ring.

Let $V$ be a finitely generated vector space over $K$.

Then $V$ has a finite basis.

Proof

This follows from Vector Space has Basis Between Linearly Independent Set and Finite Spanning Set.

It suffices to find:

A linearly independent subset $L\subset V$

A finite generator $S\subset V$

with $L\subset S$.

By Empty Set is Linearly Independent, we make take $L = \O$ and $S$ any finite generator, which exists because $V$ is finitely generated.

$\blacksquare$

Also see

• Vector Space has Basis, which does not assume that $V$ is finitely generated

Sources

• 1965: Seth Warner: Modern Algebra ... (previous) ... (next): Chapter $\text {V}$: Vector Spaces: $\S 27$. Subspaces and Bases: Theorem $27.8$