----- > [!proposition] Proposition. ([[every generating set contains a basis]]) > Let $k$ be a [[field]] and $V$ a $k$-[[vector space]]. Then every [[submodule generated by a subset|generating set]] of $V$ contains a [[basis]] of $V$. ^proposition > [!specialization] Statement for finite-dimensional vector spaces. Every [[submodule generated by a subset|spanning]] list in a finite dimensional [[vector space]] $V$ can be reduced to a [[basis]] of $V$. > [!proof] Proof for finite-dimensional vector spaces. > # Algorithm > Suppose $B:=v_1, \dots, v_n$ [[spans]] $V$. We want to remove some of the [[vector]]s from $v_1, \dots, v_n$ so that the remaining form a [[basis]] of $V$. The algorithm is described below. > > #### Step $1$ > If $v_1 = 0$, delete $v_1$ from $B$. (Else leave $B$ unchanged.) > > #### Step $j$ > If $v_j \in \span(v_1, \dots, v_{n-1})$, delete $v_j$ from $B$. (Else leave $B$ unchanged.) > > Stop the process after step $n$, getting a list $B$. $B$ [[spans]] $V$ because we have only removed redundant [[vector]]s. In fact, we have removed *all* redundant vectors and so [[linearly independent|linear independence]] follows from the (contrapositive of the) [[redundant vector lemma]]. ^specialization ----- #### ---- #### 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 > ```