no goals
ι : Type u'
ι' : Type ?u.201811
R : Type u_2
K : Type ?u.201817
M : Type u_1
M' : Type ?u.201823
M'' : Type ?u.201826
V : Type u
V' : Type ?u.201831
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) ↔ Disjoint (Finsupp.supported R R s) (LinearMap.ker (Finsupp.total M M R id))
apply @linearIndependent_comp_subtype_disjoint _ _ _ id