Spanning list of the right length is a basis (LADR 2.42)

• Spanning list of the right length is a basis (LADR 2.42) #Card
  • 長さ $\dim V$ の生成リストについて何が言えるか？

Back

命題. $V$ が有限次元のとき、長さ $\dim V$ の任意の生成リストは $V$ の基底。

証明: 生成リストは基底に削減できる（cards/linear-algebra/prop-2-30）が、どの基底も長さ $\dim V$ なので削減は自明（何も削られない）。よって元のリストが既に基底。∎

双対: 独立リスト版は cards/linear-algebra/prop-2-38。まとめると「長さが $\dim V$ なら、独立か生成のどちらか一方を確認すれば基底」。

Lean

basisOfTopLeSpanOfCardEqFinrank。