case a.h
l : Type ?u.832218
m : Type u_1
n : Type u_2
o : Type ?u.832227
m' : o → Type ?u.832232
n' : o → Type ?u.832237
R : Type ?u.832240
S : Type ?u.832243
α : Type v
β : Type w
γ : Type ?u.832250
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
w : m → α
v : n → α
i✝ : m
x✝ : n
⊢ vecMulVec w v i✝ x✝ = (col w ⬝ row v) i✝ x✝
l : Type ?u.832218
m : Type u_1
n : Type u_2
o : Type ?u.832227
m' : o → Type ?u.832232
n' : o → Type ?u.832237
R : Type ?u.832240
S : Type ?u.832243
α : Type v
β : Type w
γ : Type ?u.832250
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
w : m → α
v : n → α
⊢ vecMulVec w v = col w ⬝ row v
ext
case a.h
l : Type ?u.832218
m : Type u_1
n : Type u_2
o : Type ?u.832227
m' : o → Type ?u.832232
n' : o → Type ?u.832237
R : Type ?u.832240
S : Type ?u.832243
α : Type v
β : Type w
γ : Type ?u.832250
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
w : m → α
v : n → α
i✝ : m
x✝ : n
⊢ ↑of (fun x y => w x * v y) i✝ x✝ = col w i✝ PUnit.unit * row v PUnit.unit x✝
case a.h
l : Type ?u.832218
m : Type u_1
n : Type u_2
o : Type ?u.832227
m' : o → Type ?u.832232
n' : o → Type ?u.832237
R : Type ?u.832240
S : Type ?u.832243
α : Type v
β : Type w
γ : Type ?u.832250
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
w : m → α
v : n → α
i✝ : m
x✝ : n
⊢ vecMulVec w v i✝ x✝ = (col w ⬝ row v) i✝ x✝
simp only [vecMulVec, mul_apply, Fintype.univ_punit, Finset.sum_singleton]
no goals
case a.h
l : Type ?u.832218
m : Type u_1
n : Type u_2
o : Type ?u.832227
m' : o → Type ?u.832232
n' : o → Type ?u.832237
R : Type ?u.832240
S : Type ?u.832243
α : Type v
β : Type w
γ : Type ?u.832250
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
w : m → α
v : n → α
i✝ : m
x✝ : n
⊢ ↑of (fun x y => w x * v y) i✝ x✝ = col w i✝ PUnit.unit * row v PUnit.unit x✝
rfl