∀ {R : Type u_1} [inst : CommSemiring R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  (p : Polynomial (Matrix n n R)) (i j : n) (k : ℕ), (matPolyEquiv.symm p i j).coeff k = p.coeff k i j