no goals
ι : Type u'
ι' : Type ?u.36281
R : Type u_1
K : Type ?u.36287
M : Type u_2
M' : Type ?u.36293
M'' : Type ?u.36296
V : Type u
V' : Type ?u.36301
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
inst✝ : Fintype ι
⊢ LinearIndependent R v ↔
    LinearMap.ker (↑(LinearMap.lsum R (fun x => R) ℕ) fun i => LinearMap.smulRight LinearMap.id (v i)) = ⊥
simp [Fintype.linearIndependent_iff, LinearMap.ker_eq_bot', funext_iff]