Linearly dependent (LADR 2.17)

• Linearly dependent (LADR 2.17) #Card
  • 線形従属の定義は？従属になる典型パターンを2つ挙げよ。

Back

定義. 線形独立でないこと。つまり、すべては $0$ でない $a_1,\dots,a_m\in\mathbf{F}$ が存在して $a_1v_1+\cdots+a_mv_m=0$。

典型パターン（例 2.18）:

1. あるベクトルが他のベクトルたちの線形結合 → 従属（移項して係数 $-1$）。
2. $0$ ベクトルを含むリストは常に従属（1. の特別な場合）。

例: $(2,3,1),(1,-1,2),(7,3,c)$ が $\mathbf{F}^3$ で従属 $\iff c=8$。

Lean

¬ LinearIndependent F v。存在形の言い換えは Fintype.not_linearIndependent_iff。