no goals
ι : Type u_1
ι' : Type ?u.35738
R : Type u_2
R₂ : Type ?u.35744
K : Type ?u.35747
M : Type u_3
M' : Type ?u.35753
M'' : Type ?u.35756
V : Type u
V' : Type ?u.35761
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b b₁ : Basis ι R M
i : ι
c : R
x : M
v : ι →₀ R
⊢ ↑(LinearEquiv.symm b.repr) v = ↑(LinearEquiv.symm b.repr) (Finsupp.sum v Finsupp.single)
simp
no goals
ι : Type u_1
ι' : Type ?u.35738
R : Type u_2
R₂ : Type ?u.35744
K : Type ?u.35747
M : Type u_3
M' : Type ?u.35753
M'' : Type ?u.35756
V : Type u
V' : Type ?u.35761
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b b₁ : Basis ι R M
i : ι
c : R
x : M
v : ι →₀ R
⊢ ↑(LinearEquiv.symm b.repr) (Finsupp.sum v Finsupp.single) =
    ∑ i in v.support, ↑(LinearEquiv.symm b.repr) (Finsupp.single i (↑v i))
rw [Finsupp.sum, LinearEquiv.map_sum]
no goals
ι : Type u_1
ι' : Type ?u.35738
R : Type u_2
R₂ : Type ?u.35744
K : Type ?u.35747
M : Type u_3
M' : Type ?u.35753
M'' : Type ?u.35756
V : Type u
V' : Type ?u.35761
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b b₁ : Basis ι R M
i : ι
c : R
x : M
v : ι →₀ R
⊢ ∑ i in v.support, ↑(LinearEquiv.symm b.repr) (Finsupp.single i (↑v i)) = ↑(Finsupp.total ι M R ↑b) v
simp [repr_symm_single, Finsupp.total_apply, Finsupp.sum]