∀ {n : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type u_3} [inst_2 : CommRing R]
  (M : Matrix n n (Polynomial R)) (r : R),
  Polynomial.eval r M.det = (Polynomial.eval ((Matrix.scalar n) r) (matPolyEquiv M)).det