Tensor Product of Matrices

T.V.H. Prathamesh 📧

January 18, 2016

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.

License

BSD License

Topics

Session Matrix_Tensor

Depends on

Used by

Cite

× 
@article{Matrix_Tensor-AFP,
  author  = {T.V.H. Prathamesh},
  title   = {Tensor Product of Matrices},
  journal = {Archive of Formal Proofs},
  month   = {January},
  year    = {2016},
  note    = {\url{https://isa-afp.org/entries/Matrix_Tensor.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: