α : Type u_3
β : Type ?u.28934
γ : Type ?u.28937
m : Type u_1
n : Type u_2
R : Type ?u.28946
A B C : Matrix m n α
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Semiring α
inst✝³ : Semiring R
inst✝² : Module R α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
v : m → α
w : n → α
⊢ vecMul v (A ⊙ B) ⬝ᵥ w = ∑ y : n, ∑ x : m, ((diagonal v ⬝ A) ⊙ (B ⬝ diagonal w)) x y
α : Type u_3
β : Type ?u.28934
γ : Type ?u.28937
m : Type u_1
n : Type u_2
R : Type ?u.28946
A B C : Matrix m n α
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Semiring α
inst✝³ : Semiring R
inst✝² : Module R α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
v : m → α
w : n → α
⊢ vecMul v (A ⊙ B) ⬝ᵥ w = trace (diagonal v ⬝ A ⬝ (B ⬝ diagonal w)ᵀ)
rw [← sum_hadamard_eq, Finset.sum_comm]
no goals
α : Type u_3
β : Type ?u.28934
γ : Type ?u.28937
m : Type u_1
n : Type u_2
R : Type ?u.28946
A B C : Matrix m n α
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Semiring α
inst✝³ : Semiring R
inst✝² : Module R α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
v : m → α
w : n → α
⊢ vecMul v (A ⊙ B) ⬝ᵥ w = ∑ y : n, ∑ x : m, ((diagonal v ⬝ A) ⊙ (B ⬝ diagonal w)) x y
simp [dotProduct, vecMul, Finset.sum_mul, mul_assoc]