ι : Type u_2
ι' : Type ?u.659117
R : Type u_3
R₂ : Type ?u.659123
K : Type ?u.659126
M : Type u_1
M' : Type ?u.659132
M'' : Type ?u.659135
V : Type u
V' : Type ?u.659140
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Fintype ι
b : Basis ι R M
u : M
⊢ ∑ i : ι, ↑(equivFun b) u i • ↑b i = ↑(Finsupp.total ι M R ↑b) (↑b.repr u)
ι : Type u_2
ι' : Type ?u.659117
R : Type u_3
R₂ : Type ?u.659123
K : Type ?u.659126
M : Type u_1
M' : Type ?u.659132
M'' : Type ?u.659135
V : Type u
V' : Type ?u.659140
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Fintype ι
b : Basis ι R M
u : M
⊢ ∑ i : ι, ↑(equivFun b) u i • ↑b i = u
conv_rhs => rw [← b.total_repr u]
no goals
ι : Type u_2
ι' : Type ?u.659117
R : Type u_3
R₂ : Type ?u.659123
K : Type ?u.659126
M : Type u_1
M' : Type ?u.659132
M'' : Type ?u.659135
V : Type u
V' : Type ?u.659140
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Fintype ι
b : Basis ι R M
u : M
⊢ ∑ i : ι, ↑(equivFun b) u i • ↑b i = ↑(Finsupp.total ι M R ↑b) (↑b.repr u)
simp [Finsupp.total_apply, Finsupp.sum_fintype, b.equivFun_apply]