English
A variant of the dependence criterion expressed with Finsupp.LinearCombination unfolded.
Русский
Вариант критерия зависимости через раскрытие Finsupp.LinearCombination.
LaTeX
$$$\\\\neg \\\\mathrm{LinearIndepOn}_R v s \\\\iff \\\\exists f,g : ι \\to_0 R, f \\\\in Finsupp.supported R R s \\\\land g \\\\in Finsupp.supported R R s \\\\land \\\\sum i \\\\in f.support, f i \\, v i = \\\\sum i \\\\in g.support, g i \\, v i \\\\land f \\neq g.$$$
Lean4
/-- A version of `linearDepOn_iff'ₛ` with `Finsupp.linearCombination` unfolded. -/
theorem linearDepOn_iffₛ :
¬LinearIndepOn R v s ↔
∃ f g : ι →₀ R,
f ∈ Finsupp.supported R R s ∧
g ∈ Finsupp.supported R R s ∧ ∑ i ∈ f.support, f i • v i = ∑ i ∈ g.support, g i • v i ∧ f ≠ g :=
linearDepOn_iff'ₛ
