-----
> [!proposition] Proposition. ([[every vector space has a basis]])
> Let $R=k$ be a [[field]] and let $V$ be a $k$-[[vector space]]. Let $S$ be a [[linearly independent]] set of [[vector|vectors]] of $V$. Then there exists a [[basis]] $B$ of $V$ containing $S$.
>
> In particular, $V$ is [[free module|free]] as a $k$-[[module]].
^proposition
> [!specialization] Statement for finite-dimensional vector spaces.
Every [[vector space#Finite-Dimensional Vector Space|finite-dimensional vector space]] $V$ has a [[basis]]: by definition $V$ contains a [[submodule generated by a subset|spanning set]]; then the result follows from [[every generating set contains a basis]].
>
(This proof avoids [[Zorn's lemma]], and hence the [[Axiom of Choice]].)
> [!proof]- Proof. ([[every vector space has a basis]])
> Start with [[every linearly independent subset completes to a maximal linearly independent subset]] to get a [[maximal]] [[linearly independent]] set $B$ containing $S$. Is $B$ a [[basis]]? Yes, by [[vector space basis iff maximal linearly independent]].
>
In particular, by [[module is free iff admits basis]] we have that $V$ is free as a $k$-[[module]].
-----
####
----
#### References
> [!backlink]
> ```dataview
> TABLE rows.file.link as "Further Reading"
> FROM [[]]
> FLATTEN file.tags as Tag
> WHERE Tag = "#definition" OR Tag = "#theorem" OR Tag = "#MOC" OR Tag = "#proposition" OR Tag = "#axiom"
> GROUP BY Tag
> ```
> [!frontlink]
> ```dataview
> TABLE rows.file.link as "Further Reading"
> FROM outgoing([[]])
> FLATTEN file.tags as Tag
> WHERE Tag = "#definition" OR Tag = "#theorem" OR Tag = "#MOC" OR Tag = "#proposition" OR Tag = "#axiom"
> GROUP BY Tag
> ```