linearIndepOn_iff_linearCombinationOnₛ

English

LinearIndepOn R v s is equivalent to the injectivity of the linear map Finsupp.linearCombinationOn ι M R v s.

Русский

LinearIndepOn R v s эквивалентно инъективности линейного отображения Finsupp.linearCombinationOn ι M R v s.

LaTeX

$$$$ \operatorname{LinearIndepOn}_R(v,s) \iff \operatorname{Injective}\bigl( Finsupp.linearCombinationOn\, \iota\, M\, R\, v\, s \bigr). $$$$

Lean4

theorem linearIndepOn_iff_linearCombinationOnₛ :
    LinearIndepOn R v s ↔ Injective (Finsupp.linearCombinationOn ι M R v s) :=
  by
  rw [← linearIndependent_restrict_iff]
  simp [LinearIndependent, Finsupp.linearCombination_restrict]

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