### Abstract

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.

January 18, 2016

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.