Every spanning list contains a basis (LADR 2.30, 2.31)
- Every spanning list contains a basis (LADR 2.30, 2.31) #Card
- 生成リストから基底を得る方法は？そこから出る基底の存在定理は？
命題 (2.30). 任意の生成リストは、いくつかのベクトルを削って基底にできる。
手続き: $v_1,\dots,v_n$ を順に見て、$v_k\in\operatorname{span}(v_1,\dots,v_{k-1})$ なら削除（$v_1=0$ なら削除）。削除しても span は不変（cards/linear-algebra/prop-2-19 後半）。最後に残るリストは「どのベクトルも前の span に入らない」ので独立（同補題の対偶）。
系 (2.31). 有限次元ベクトル空間は基底を持つ（定義より生成リストがあり、それを削ればよい）。
例: $(1,2),(3,6),(4,7),(5,9)$ → 第2・第4を削除 → 基底 $(1,2),(4,7)$。
Basis.exists_basis（FiniteDimensional 下では Module.finBasis など）。