simp only [←inner_basis_dualProj, inner_dualBasis_basis, eq_comm]
ι : Type u_2
K : Type u_1
X : Type u_3
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : RCLike K
inst✝ : FinVec ι K X
i j : ι
⊢ ℼ' i ⅇ' j = if i = j then 1 else 0
no goals