not_linearIndependent_iff — Mathlib

English

For a finite index set ι, not LinearIndependent R v is equivalent to the existence of a finite index subset s and a nontrivial g: ι → R with ∑ i∈s g(i) v(i) = 0 and some g(i) ≠ 0.

Русский

Для конечного множества индексов существует s и не тривиальные коэффициенты g так, чтобы сумма линейной комбинации давала нулю.

LaTeX

$$$$\\neg\\operatorname{LinearIndependent}_R(v) \\iff \\exists s:\\mathrm{Finset}\\,\\ι,\\exists g:\\ι\\to R,\\; \\Big(\\sum_{i\\in s} g(i)\\,v(i) = 0\\Big) \\land \\exists i\\in s,\\; g(i)\\neq 0.$$$$

Lean4

theorem not_linearIndependent_iff [Fintype ι] :
    ¬LinearIndependent R v ↔ ∃ g : ι → R, ∑ i, g i • v i = 0 ∧ ∃ i, g i ≠ 0 := by
  simpa using not_iff_not.2 Fintype.linearIndependent_iff

Похожие утверждения