[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
m : Type u_4
n : Type u_5
R : Type u_6
A B C : Matrix m n α
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
M : Matrix n n α
⊢ M ⊙ 1 = diagonal fun i => M i i
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u_1
β : Type u_2
γ : Type u_3
m : Type u_4
n : Type u_5
R : Type u_6
A B C : Matrix m n α
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
M : Matrix n n α
i j : n
⊢ (M ⊙ 1) i j = diagonal (fun i => M i i) i j
[PROOFSTEP]
by_cases h : i = j
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
m : Type u_4
n : Type u_5
R : Type u_6
A B C : Matrix m n α
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
M : Matrix n n α
i j : n
h : i = j
⊢ (M ⊙ 1) i j = diagonal (fun i => M i i) i j
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
m : Type u_4
n : Type u_5
R : Type u_6
A B C : Matrix m n α
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
M : Matrix n n α
i j : n
h : ¬i = j
⊢ (M ⊙ 1) i j = diagonal (fun i => M i i) i j
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
m : Type u_4
n : Type u_5
R : Type u_6
A B C : Matrix m n α
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
M : Matrix n n α
⊢ 1 ⊙ M = diagonal fun i => M i i
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u_1
β : Type u_2
γ : Type u_3
m : Type u_4
n : Type u_5
R : Type u_6
A B C : Matrix m n α
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
M : Matrix n n α
i j : n
⊢ (1 ⊙ M) i j = diagonal (fun i => M i i) i j
[PROOFSTEP]
by_cases h : i = j
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
m : Type u_4
n : Type u_5
R : Type u_6
A B C : Matrix m n α
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
M : Matrix n n α
i j : n
h : i = j
⊢ (1 ⊙ M) i j = diagonal (fun i => M i i) i j
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
m : Type u_4
n : Type u_5
R : Type u_6
A B C : Matrix m n α
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
M : Matrix n n α
i j : n
h : ¬i = j
⊢ (1 ⊙ M) i j = diagonal (fun i => M i i) i j
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
m : Type u_4
n : Type u_5
R : Type u_6
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)ᵀ)
[PROOFSTEP]
rw [← sum_hadamard_eq, Finset.sum_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
m : Type u_4
n : Type u_5
R : Type u_6
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
[PROOFSTEP]
simp [dotProduct, vecMul, Finset.sum_mul, mul_assoc]
