Matrix_Multiplication_is_Associative

import Mathlib.Analysis.Complex.Basic

theorem Matrix_Multiplication_is_Associative {R : Type _} [Ring R] {m n p q : ℕ} (A : Matrix (Fin m) (Fin n) R) (B : Matrix (Fin n) (Fin p) R) (C : Matrix (Fin p) (Fin q) R) : A * B * C = A * (B * C) := by sorry