Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: Tensor Product of Matrices


view this post on Zulip Email Gateway (Aug 22 2022 at 12:09):

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: Mar 28 2024 at 16:17 UTC