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

- Computer science/Data structures
- Mathematics/Algebra

### Session Matrix_Tensor

- Matrix_Tensor

### Depends on

- Executable Matrix Operations on Matrices of Arbitrary Dimensions

### Used by

- Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information
- Knot Theory

## Cite

×

Matrix_Tensor-AFP

    @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:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- Jan 19, 2016 : Isabelle2015
- Jan 18, 2016 : Isabelle2015