ι : Type u'
ι' : Type ?u.455472
R : Type u_2
K : Type ?u.455478
M : Type u_1
M' : Type ?u.455484
M'' : Type ?u.455487
V : Type u
V' : Type ?u.455492
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
i : ι
x : { x // x ∈ span R (range v) }
hx : ↑x = v i
⊢ ↑(Finsupp.total ι M R v) (Finsupp.single i 1) = ↑x
ι : Type u'
ι' : Type ?u.455472
R : Type u_2
K : Type ?u.455478
M : Type u_1
M' : Type ?u.455484
M'' : Type ?u.455487
V : Type u
V' : Type ?u.455492
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
i : ι
x : { x // x ∈ span R (range v) }
hx : ↑x = v i
⊢ ↑(repr hv) x = Finsupp.single i 1
apply hv.repr_eq
no goals
ι : Type u'
ι' : Type ?u.455472
R : Type u_2
K : Type ?u.455478
M : Type u_1
M' : Type ?u.455484
M'' : Type ?u.455487
V : Type u
V' : Type ?u.455492
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
i : ι
x : { x // x ∈ span R (range v) }
hx : ↑x = v i
⊢ ↑(Finsupp.total ι M R v) (Finsupp.single i 1) = ↑x
simp [Finsupp.total_single, hx]