linearIndependent_iff_injective_finsuppLinearCombination

English

Linear independence of v is equivalent to the injectivity of the linear combination map Finsupp.linearCombination R v.

Русский

Линейная независимость v эквивалентна инъективности отображения линейной комбинации, заданного Finsupp.linearCombination R v.

LaTeX

$$$\\operatorname{LinearIndependent}(R,v) \\iff \\operatorname{Injective}\\left( Finsupp.linearCombination\\;R\\;v \\right)$$$

Lean4

theorem linearIndependent_iff_injective_finsuppLinearCombination :
    LinearIndependent R v ↔ Injective (Finsupp.linearCombination R v) :=
  Iff.rfl

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