no goals
R : Type v
n : Type w
inst✝² : Semiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → R
i : n
⊢ v ⬝ᵥ ↑(LinearMap.stdBasis R (fun x => R) i) 1 = v i
rw [dotProduct_stdBasis_eq_mul, mul_one]