rw [Matrix.mul_kronecker_mul]
ι : Type ?u.36909
R : Type u_3
l : Type u_1
m : Type u_2
n : Type u_6
p : Type u_4
q : Type u_5
r : Type u_7
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix l m R
B : Matrix p q R
C : Matrix m n R
D : Matrix q r R
⊢ kroneckerMap (fun x x_1 => x * x_1) A B * kroneckerMap (fun x x_1 => x * x_1) C D =
    kroneckerMap (fun x x_1 => x * x_1) (A * C) (B * D)
no goals