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✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Fintype ι
l : Dual R M
i : ι
⊢ ↑(equivFun (dualBasis b)) l i = ↑l (↑b i)
rw [Basis.equivFun_apply, dualBasis_repr]