∀ {R : Type u_1} [inst : CommSemiring R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (p : Polynomial R)
  (M : Matrix n n (Polynomial R)),
  matPolyEquiv (p • M) = Polynomial.map (algebraMap R (Matrix n n R)) p * matPolyEquiv M