sorry_proof
ι : 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 : ι
x : X
⊢ ⟪x, ⅇ' i⟫_K = ℼ i x
no goals