Linearly independent list of the right length is a basis (LADR 2.38)

• Linearly independent list of the right length is a basis (LADR 2.38) #Card
  • 長さ $\dim V$ の線形独立リストについて何が言えるか？なぜ生成性の確認が省けるのか？

Back

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

証明: 独立リストは基底に拡張できる（cards/linear-algebra/prop-2-32）が、どの基底も長さ $\dim V$ なので、拡張は自明（何も足されない）。よって元のリストが既に基底。∎

使い方（例 2.40）: $(5,7),(4,3)$ は互いにスカラー倍でない→独立、長さ2 $=\dim\mathbf{F}^2$ →基底。生成性の検証を省略できるのが実用上の価値。

双対: 生成リスト版は cards/linear-algebra/prop-2-42。

Lean

LinearIndependent.basisOfLinearIndependentOfCardEqFinrank。