case h
l : Type ?u.881533
m : Type ?u.881536
n : Type u_1
o : Type ?u.881542
m' : o → Type ?u.881547
n' : o → Type ?u.881552
R : Type u_2
S : Type ?u.881558
α : Type v
β : Type w
γ : Type ?u.881565
inst✝³ : NonUnitalNonAssocSemiring α
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
⊢ vecMul (Pi.single j x) (diagonal v) i = Pi.single j (x * v j) i
l : Type ?u.881533
m : Type ?u.881536
n : Type u_1
o : Type ?u.881542
m' : o → Type ?u.881547
n' : o → Type ?u.881552
R : Type u_2
S : Type ?u.881558
α : Type v
β : Type w
γ : Type ?u.881565
inst✝³ : NonUnitalNonAssocSemiring α
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
⊢ vecMul (Pi.single j x) (diagonal v) = Pi.single j (x * v j)
ext i
case h
l : Type ?u.881533
m : Type ?u.881536
n : Type u_1
o : Type ?u.881542
m' : o → Type ?u.881547
n' : o → Type ?u.881552
R : Type u_2
S : Type ?u.881558
α : Type v
β : Type w
γ : Type ?u.881565
inst✝³ : NonUnitalNonAssocSemiring α
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
⊢ Pi.single j x i * v i = Pi.single j (x * v j) i
case h
l : Type ?u.881533
m : Type ?u.881536
n : Type u_1
o : Type ?u.881542
m' : o → Type ?u.881547
n' : o → Type ?u.881552
R : Type u_2
S : Type ?u.881558
α : Type v
β : Type w
γ : Type ?u.881565
inst✝³ : NonUnitalNonAssocSemiring α
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
⊢ vecMul (Pi.single j x) (diagonal v) i = Pi.single j (x * v j) i
rw [vecMul_diagonal]
no goals
case h
l : Type ?u.881533
m : Type ?u.881536
n : Type u_1
o : Type ?u.881542
m' : o → Type ?u.881547
n' : o → Type ?u.881552
R : Type u_2
S : Type ?u.881558
α : Type v
β : Type w
γ : Type ?u.881565
inst✝³ : NonUnitalNonAssocSemiring α
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
⊢ Pi.single j x i * v i = Pi.single j (x * v j) i
exact Pi.apply_single (fun i x => x * v i) (fun i => MulZeroClass.zero_mul _) j x i