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: Nov 21 2024 at 12:39 UTC