Trace of tensor product

Stream: Is there code for X?

[Antoine Labelle]

Do we have in mathlib the fact that linear_map.trace (tensor_product.map f g) = (linear_map.trace f)*(linear_map.trace g)?

[Filippo A. E. Nuccio]

I don't know, but have you had a look at https://leanprover-community.github.io/mathlib_docs/data/matrix/kronecker.html#matrix.kronecker_map ? If you can connect the matrix tensor_product.map to the Kronecker product of the two matrices (which should be of independent interest), this would seem the right place to insert the result.