Basis (LADR 2.26)

• Basis (LADR 2.26) #Card
  • $V$ の基底の定義と、標準基底の例を2つ挙げよ。

Back

定義. $V$ の基底＝線形独立かつ $V$ を生成するリスト。

標準例（例 2.27）:

• $\mathbf{F}^n$ の標準基底 $(1,0,\dots,0),(0,1,0,\dots,0),\dots,(0,\dots,0,1)$。
• $\mathcal{P}_m(\mathbf{F})$ の標準基底 $1,z,\dots,z^m$。

非例: 独立だが生成しない（$\mathbf{F}^3$ の $(1,2,-4),(7,-5,6)$）／生成するが独立でない（$\mathbf{F}^2$ の $(1,2),(3,5),(4,13)$）—「小さすぎず大きすぎず」の両立が基底。

Lean

Basis ι F V（Mathlib では「係数への線形同型 V ≃ₗ (ι →₀ F)」として定義）。