case h₀
R : Type v
n : Type w
inst✝² : Semiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → R
c : R
i : n
⊢ ∀ (b : n), b ∈ Finset.univ → b ≠ i → v b * ↑(LinearMap.stdBasis R (fun x => R) i) c b = 0

case h₁
R : Type v
n : Type w
inst✝² : Semiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → R
c : R
i : n
⊢ ¬i ∈ Finset.univ → v i * ↑(LinearMap.stdBasis R (fun x => R) i) c i = 0
R : Type v
n : Type w
inst✝² : Semiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → R
c : R
i : n
⊢ v ⬝ᵥ ↑(LinearMap.stdBasis R (fun x => R) i) c = v i * c
rw [dotProduct, Finset.sum_eq_single i, LinearMap.stdBasis_same]
case h₁
R : Type v
n : Type w
inst✝² : Semiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → R
c : R
i : n
⊢ ¬i ∈ Finset.univ → v i * ↑(LinearMap.stdBasis R (fun x => R) i) c i = 0
case h₀
R : Type v
n : Type w
inst✝² : Semiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → R
c : R
i : n
⊢ ∀ (b : n), b ∈ Finset.univ → b ≠ i → v b * ↑(LinearMap.stdBasis R (fun x => R) i) c b = 0

case h₁
R : Type v
n : Type w
inst✝² : Semiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → R
c : R
i : n
⊢ ¬i ∈ Finset.univ → v i * ↑(LinearMap.stdBasis R (fun x => R) i) c i = 0
exact fun _ _ hb => by rw [LinearMap.stdBasis_ne _ _ _ _ hb, MulZeroClass.mul_zero]
no goals
case h₁
R : Type v
n : Type w
inst✝² : Semiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → R
c : R
i : n
⊢ ¬i ∈ Finset.univ → v i * ↑(LinearMap.stdBasis R (fun x => R) i) c i = 0
exact fun hi => False.elim (hi <| Finset.mem_univ _)
no goals
R : Type v
n : Type w
inst✝² : Semiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → R
c : R
i x✝¹ : n
x✝ : x✝¹ ∈ Finset.univ
hb : x✝¹ ≠ i
⊢ v x✝¹ * ↑(LinearMap.stdBasis R (fun x => R) i) c x✝¹ = 0
rw [LinearMap.stdBasis_ne _ _ _ _ hb, MulZeroClass.mul_zero]