no goals
ι : Type u'
ι' : Type ?u.440821
R : Type u_2
K : Type ?u.440827
M : Type u_1
M' : Type ?u.440833
M'' : Type ?u.440836
V : Type u
V' : Type ?u.440841
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
⊢ LinearMap.ker (repr hv) = ⊥
rw [LinearIndependent.repr, LinearEquiv.ker]