∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {m' : Type u_6} {n' : Type u_7} {o' : Type u_8} (R : Type u_11)
  (A : Type u_12) [inst : Semiring R] [inst_1 : Semiring A] [inst_2 : Module R A] [inst_3 : Fintype n]
  [inst_4 : Fintype n'] (eₘ : m ≃ m') (eₙ : n ≃ n') (eₒ : o ≃ o') (M : Matrix m n A) (N : Matrix n o A),
  (Matrix.reindexLinearEquiv R A eₘ eₙ) M * (Matrix.reindexLinearEquiv R A eₙ eₒ) N =
    (Matrix.reindexLinearEquiv R A eₘ eₒ) (M * N)