`BookProof.ChapterA3.Treal_mul` (A B : Matrix (Fin 2) (Fin 2) ℂ) : Treal (A * B) = Treal A * Treal B

Initializing...

`BookProof.ChapterA3.Treal_mul` (A B : Matrix (Fin 2) (Fin 2) ℂ) : Treal (A * B) = Treal A * Treal B · Prove2Me