linearIndepOn_iff_linearCombinationOn

English

The non-independence on a Finset is equivalent to the existence of a finite indexed nontrivial relation ∑ i∈s g(i) v(i) = 0 with some g(i) ≠ 0.

Русский

Не независимость на Finset эквивалентна существованию ненулевой конечной линейной зависимости ∑ i∈s g(i) v(i) = 0.

LaTeX

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

Lean4

theorem linearIndepOn_iff_linearCombinationOn :
    LinearIndepOn R v s ↔ (LinearMap.ker <| Finsupp.linearCombinationOn ι M R v s) = ⊥ :=
  linearIndepOn_iff_linearCombinationOnₛ.trans <| LinearMap.ker_eq_bot (M := Finsupp.supported R R s).symm

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