The Exercise

An operator $A$ on one system and an operator $B$ on another, written as matrices in chosen bases, give the operator $A \otimes B$ on the joint system, and its matrix is the Kronecker product of the two matrices. The exercise asks to show that complex conjugation, taken entry by entry, distributes over this product: conjugating the matrix of $A \otimes B$ gives the same matrix as conjugating $A$ and $B$ first and then taking their tensor product.^✦

Matrices and Their Conjugates

The scalars are the elements of a set $R$ with a commutative product, $rs = sr$, and a conjugation $r \mapsto r^*$, an involution that reverses products: $$(r^*)^* = r, \qquad (rs)^* = s^* r^* .$$(1)

The Kronecker product $A \otimes B$ of a matrix $A$ with entries $A_{ij}$ and a matrix $B$ with entries $B_{kl}$, both over $R$ and of any shapes, is the matrix whose entry in row $(i,k)$ and column $(j,l)$ is $$(A \otimes B)_{(i,k),(j,l)} = A_{ij}\, B_{kl} .$$(2)

The conjugate $A^*$ of a matrix $A$ over $R$ is the matrix of the same shape whose entries are the conjugates of those of $A$: $$(A^*)_{ij} = (A_{ij})^* .$$(3)

The Claim

For complex matrices, with $r^*$ the complex conjugate of $r$, this is the exercise.

What Is Checked

The claim is stated over two constructions on matrices with entries in $R$: the Kronecker product (2) and the conjugate (3), for factors of any shapes, square or not, and for any scalars with the properties (1).

What the library proves about these constructions is (4).