rw [linearIndependent_iff]
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
⊢ LinearIndependent (ι := ↑s) R (s.restrict f) ↔ ∀ (l : ι →₀ R), (Finsupp.total ι M R f) l = 0 → ↑l.support ⊆ s → l = 0
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
⊢ (∀ (l : ↑s →₀ R), (Finsupp.total (↑s) M R (s.restrict f)) l = 0 → l = 0) ↔
    ∀ (l : ι →₀ R), (Finsupp.total ι M R f) l = 0 → ↑l.support ⊆ s → l = 0