R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : _root_.Finite ι
b : Basis ι R M
f : ι →₀ R
i : ι
this : DecidableEq ι
⊢ ↑(↑(Finsupp.total ι (Dual R M) R (coord b)) f) (↑b i) = ↑f i
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : _root_.Finite ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ ↑(↑(Finsupp.total ι (Dual R M) R (coord b)) f) (↑b i) = ↑f i
haveI := Classical.decEq ι
no goals
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : _root_.Finite ι
b : Basis ι R M
f : ι →₀ R
i : ι
this : DecidableEq ι
⊢ ↑(↑(Finsupp.total ι (Dual R M) R (coord b)) f) (↑b i) = ↑f i
rw [← coe_dualBasis, total_dualBasis]