no goals
R : Type u_1
α : Type u_4
α' : Type ?u.49841
β : Type u_5
β' : Type ?u.49847
γ : Type u_6
γ' : Type ?u.49853
l : Type ?u.49856
m : Type u_2
n : Type u_3
p : Type ?u.49865
q : Type ?u.49868
r : Type ?u.49871
l' : Type ?u.49874
m' : Type ?u.49877
n' : Type ?u.49880
p' : Type ?u.49883
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : AddCommMonoid γ
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : Module R γ
f : α →ₗ[R] β →ₗ[R] γ
A : Matrix m m α
B : Matrix n n β
⊢ trace (↑(↑(kroneckerMapBilinear f) A) B) = ↑(↑f (trace A)) (trace B)
simp_rw [Matrix.trace, Matrix.diag, kroneckerMapBilinear_apply_apply, LinearMap.map_sum₂,
  map_sum, ← Finset.univ_product_univ, Finset.sum_product, kroneckerMap_apply]