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✝ : _root_.Finite ι
i j : ι
⊢ ↑(↑(LinearMap.comp (toDual (dualBasis b)) (toDual b)) (↑b i)) (↑(dualBasis b) j) =
    ↑(↑(Dual.eval R M) (↑b i)) (↑(dualBasis b) j)
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✝ : _root_.Finite ι
⊢ LinearMap.comp (toDual (dualBasis b)) (toDual b) = Dual.eval R M
refine' b.ext fun i => b.dualBasis.ext fun j => _
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✝ : _root_.Finite ι
i j : ι
⊢ ↑(↑(LinearMap.comp (toDual (dualBasis b)) (toDual b)) (↑b i)) (↑(dualBasis b) j) =
    ↑(↑(Dual.eval R M) (↑b i)) (↑(dualBasis b) j)
rw [LinearMap.comp_apply, toDual_apply_left, coe_toDual_self, ← coe_dualBasis,
  Dual.eval_apply, Basis.repr_self, Finsupp.single_apply, dualBasis_apply_self]