∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] (i : ι) (a : 𝕜)
  (v : EuclideanSpace 𝕜 ι), inner 𝕜 v (EuclideanSpace.single i a) = a * (starRingEnd ((fun x => 𝕜) i)) (v.ofLp i)