linearIndependent_iff_injective_fintypeLinearCombination

English

If ι is finite, Linear independense of v is equivalent to the injectivity of the corresponding Fintype.linearCombination.

Русский

Если множество индексов ι конечное, линейная независимость v эквивалентна инъективности соответствующего Fintype.linearCombination.

LaTeX

$$$[Fintype\\ ι]\\;\\operatorname{LinearIndependent}(R,v) \\iff \\operatorname{Injective}\\left( Fintype.linearCombination\\;R\\;v \\right)$$$

Lean4

theorem linearIndependent_iff_injective_fintypeLinearCombination [Fintype ι] :
    LinearIndependent R v ↔ Injective (Fintype.linearCombination R v) := by
  simp [← Finsupp.linearCombination_eq_fintype_linearCombination, LinearIndependent]

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