∀ {n : Type v} [inst : DecidableEq n] [inst_1 : Fintype n] {K : Type u_1} (k : ℕ) [inst_2 : CommRing K]
  (M : Matrix n n K),
  matPolyEquiv ((↑(Polynomial.expand K k)).mapMatrix (M ^ k).charmatrix) = Polynomial.X ^ k - Polynomial.C (M ^ k)