Theorem: SciLean.inner_dualBasis_basis (SciLean/Core/Objects/FinVec.lean)

State before:
ι : Type u_3
K : Type u_1
X : Type u_2
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : RCLike K
inst✝ : FinVec ι K X
i j : ι
⊢ ⟪ⅇ' i, ⅇ j⟫_K = if i = j then 1 else 0
Tactic:
sorry_proof
State after:
no goals