`BookProof.ChapterA3.toEuclideanLin_mul4` (A B : Matrix (Fin 4) (Fin 4) ℂ) : Matrix.toEuclideanLin (A * B) = (Matrix.toEuclideanLin A) ∘ₗ (Matrix.toEuclideanLin B)

Initializing...

`BookProof.ChapterA3.toEuclideanLin_mul4` (A B : Matrix (Fin 4) (Fin 4) ℂ) : Matrix.toEuclideanLin (A * B) = (Matrix.toEuclideanLin A) ∘ₗ (Matrix.toEuclideanLin B) · Prove2Me