no goals
ι : Type u'
ι' : Type ?u.197690
R : Type u_2
K : Type ?u.197696
M : Type u_1
M' : Type ?u.197702
M'' : Type ?u.197705
V : Type u
V' : Type ?u.197710
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s : Set M
⊢ (LinearIndependent R fun x => ↑x) ↔
    ∀ (l : M →₀ R), l ∈ Finsupp.supported R R s → ↑(Finsupp.total M M R id) l = 0 → l = 0
apply @linearIndependent_comp_subtype _ _ _ id