`BookProof.ChapterA3m.swap13_kronecker` (A B C : Matrix (Fin 4) (Fin 4) ℂ) : swap13 * ((A ⊗ₖ B) ⊗ₖ C) = ((C ⊗ₖ B) ⊗ₖ A) * swap13

Initializing...

`BookProof.ChapterA3m.swap13_kronecker` (A B C : Matrix (Fin 4) (Fin 4) ℂ) : swap13 * ((A ⊗ₖ B) ⊗ₖ C) = ((C ⊗ₖ B) ⊗ₖ A) * swap13 · Prove2Me