case a.h
m : Type ?u.1456082
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
v : n → R
A : Matrix n n R
i✝ x✝ : n
⊢ ↑of (fun i j => v j * A i j) i✝ x✝ = (A ⬝ diagonal v) i✝ x✝
m : Type ?u.1456082
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
v : n → R
A : Matrix n n R
⊢ (↑of fun i j => v j * A i j) = A ⬝ diagonal v
ext
no goals
case a.h
m : Type ?u.1456082
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
v : n → R
A : Matrix n n R
i✝ x✝ : n
⊢ ↑of (fun i j => v j * A i j) i✝ x✝ = (A ⬝ diagonal v) i✝ x✝
simp [mul_comm]
no goals
m : Type ?u.1456082
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
v : n → R
A : Matrix n n R
⊢ det (A ⬝ diagonal v) = (∏ i : n, v i) * det A
rw [det_mul, det_diagonal, mul_comm]