From: Tobias Nipkow <nipkow@in.tum.de>
Tensor Product of Matrices
T.V.H. Prathamesh
In this work, the Kronecker tensor product of matrices and the proofs of some of
its properties are formalized. Properties which have been formalized include
associativity of the tensor product and the mixed-product property.
http://afp.sourceforge.net/entries/Matrix_Tensor.shtml
Enjoy!
smime.p7s
Last updated: Feb 01 2025 at 20:19 UTC