`BookProof.ChapterA3.castMat_neg_one` : (Int.castRingHom ℝ).mapMatrix (-1 : Matrix (Fin 4) (Fin 4) ℤ) = -1

Initializing...

`BookProof.ChapterA3.castMat_neg_one` : (Int.castRingHom ℝ).mapMatrix (-1 : Matrix (Fin 4) (Fin 4) ℤ) = -1 · Prove2Me