∀ {m : Type u_2} {n : Type u_3} (R : Type u_5) [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  [inst_3 : Fintype m] [inst_4 : DecidableEq m] (x : TensorProduct R (Matrix m m R) (Matrix n n R)),
  (Matrix.kroneckerAlgEquiv m n R) x = (kroneckerLinearEquiv m m n n R) x