Matrix_Mul_Distributes_over_Addition

import Mathlib.Analysis.Complex.Basic

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