case h
l : Type ?u.878832
m : Type ?u.878835
n : Type u_1
o : Type ?u.878841
m' : o → Type ?u.878846
n' : o → Type ?u.878851
R : Type u_2
S : Type ?u.878857
α : Type v
β : Type w
γ : Type ?u.878864
inst✝³ : NonUnitalNonAssocSemiring α
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
⊢ mulVec (diagonal v) (Pi.single j x) i = Pi.single j (v j * x) i
l : Type ?u.878832
m : Type ?u.878835
n : Type u_1
o : Type ?u.878841
m' : o → Type ?u.878846
n' : o → Type ?u.878851
R : Type u_2
S : Type ?u.878857
α : Type v
β : Type w
γ : Type ?u.878864
inst✝³ : NonUnitalNonAssocSemiring α
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
⊢ mulVec (diagonal v) (Pi.single j x) = Pi.single j (v j * x)
ext i
case h
l : Type ?u.878832
m : Type ?u.878835
n : Type u_1
o : Type ?u.878841
m' : o → Type ?u.878846
n' : o → Type ?u.878851
R : Type u_2
S : Type ?u.878857
α : Type v
β : Type w
γ : Type ?u.878864
inst✝³ : NonUnitalNonAssocSemiring α
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
⊢ v i * Pi.single j x i = Pi.single j (v j * x) i
case h
l : Type ?u.878832
m : Type ?u.878835
n : Type u_1
o : Type ?u.878841
m' : o → Type ?u.878846
n' : o → Type ?u.878851
R : Type u_2
S : Type ?u.878857
α : Type v
β : Type w
γ : Type ?u.878864
inst✝³ : NonUnitalNonAssocSemiring α
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
⊢ mulVec (diagonal v) (Pi.single j x) i = Pi.single j (v j * x) i
rw [mulVec_diagonal]
no goals
case h
l : Type ?u.878832
m : Type ?u.878835
n : Type u_1
o : Type ?u.878841
m' : o → Type ?u.878846
n' : o → Type ?u.878851
R : Type u_2
S : Type ?u.878857
α : Type v
β : Type w
γ : Type ?u.878864
inst✝³ : NonUnitalNonAssocSemiring α
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
⊢ v i * Pi.single j x i = Pi.single j (v j * x) i
exact Pi.apply_single (fun i x => v i * x) (fun i => MulZeroClass.mul_zero _) j x i