Every linearly independent list extends to a basis (LADR 2.32)
- Every linearly independent list extends to a basis (LADR 2.32) #Card
- 有限次元空間で、線形独立リストから基底を得る方法は？
命題. 有限次元ベクトル空間の任意の線形独立リスト $u_1,\dots,u_m$ は、ベクトルを足して基底に拡張できる。
証明の骨子: 生成リスト $w_1,\dots,w_n$ を後ろに連結した $u_1,\dots,u_m,w_1,\dots,w_n$ は生成リスト。これに cards/linear-algebra/prop-2-30 の削減手続きを適用すると、$u$ たちは独立なので誰も削られず、$u_1,\dots,u_m$ と一部の $w$ からなる基底が得られる。
双対の視点: 2.30「削って基底」⟷ 2.32「足して基底」。
例: $\mathbf{F}^3$ で $(2,3,4),(9,6,8)$ に標準基底を連結 → $(2,3,4),(9,6,8),(0,1,0)$ が基底。
Basis.extend（LinearIndependent.extend）。