linearIndependent_iffₛ — Mathlib

English

A variant of LI with Finset, involving equality of sums over Finsets implies coordinate equality.

Русский

Вариант LI с Finset: равенство сумм по Finset влечёт равенство коэффициентов на элементах Finset.

LaTeX

$$$\\operatorname{LinearIndependent}(R,v) \\iff \\forall s:\\operatorname{Finset} ι, \\forall f,g:ι→R, (\\sum_{i∈s} f_i v_i)=(\\sum_{i∈s} g_i v_i) \\to \\forall i∈s, f_i=g_i$$$

Lean4

theorem linearIndependent_iffₛ :
    LinearIndependent R v ↔ ∀ l₁ l₂, Finsupp.linearCombination R v l₁ = Finsupp.linearCombination R v l₂ → l₁ = l₂ :=
  Iff.rfl

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