not_linearIndependent_iffₛ — Mathlib

English

If the family is not linearly independent, there exist two coefficient functions witnessing a nontrivial relation, i.e., there is a finite sum with equal linear combinations but different coefficients at some index.

Русский

Если семейство латинно не линейно независимо, существуют две функции коэффициентов, дающие одну и ту же линейную комбинацию, но различающиеся на каком-либо индексе.

LaTeX

$$$\\\\neg \\\\mathrm{LinearIndependent}_R(v) \\\\iff \\\\exists f,g : \iota \\to R, \\\\Big( \\\\sum_i f(i) \\, v_i = \\\\sum_i g(i) \\, v_i \\\\land \\\\exists i, f(i) \neq g(i) \Big).$$$

Lean4

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

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