∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : NonUnitalSemiring α]
  [inst_1 : Fintype m] [inst_2 : Fintype n] (L : Matrix l m α) (M : Matrix m n α) (N : Matrix n o α),
  L * (M * N) = L * M * N