**This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.**

### 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.