∀ {m : Type u_1} {n : Type u_3} (A : Type u_2) [inst : Fintype n] [inst_1 : Fintype m] [inst_2 : Semiring A] (e : m ≃ n)
  (a b : Matrix m m A),
  (Matrix.reindexLinearEquiv A A e e) (a * b) =
    (Matrix.reindexLinearEquiv A A e e) a * (Matrix.reindexLinearEquiv A A e e) b