QuantumInfo.ForMathlib.Unitary

Let $E$ be a vector space over a field $\mathbf{k}$, and let $U$ be a unitary linear map from $E$ to $E$ ($U \in \text{unitary}(E \to_{\mathbf{k}} E)$). For any vector $v \in E$, applying the adjoint (star) of $U$ to the result of $U$ applied to $v$ returns the original vector $v$. That is, $U^*(U(v)) = v$.

Let $E$ be a vector space over a field $\mathbb{k}$, and let $U$ be a unitary linear map from $E$ to $E$. For any vector $v \in E$, applying the map $U$ to the result of its adjoint (star) map applied to $v$ yields $v$, i.e., $U(U^* v) = v$. Since $U$ is unitary, its adjoint $U^*$ is its inverse, and this statement expresses the identity $U \circ U^* = \text{id}_E$.

Let $E$ be a vector space over a field $\mathbf{k}$, let $T: E \to E$ be a linear map, and let $U$ be a unitary operator on $E$. For any scalar $\mu \in \mathbf{k}$, there exists a linear equivalence between the $\mu$-eigenspace of $T$ and the $\mu$-eigenspace of the conjugated map $U T U^*$. This equivalence maps an eigenvector $v$ of $T$ to $Uv$, and its inverse maps an eigenvector $w$ of $U T U^*$ to $U^* w$. Elements in both spaces satisfy the condition $T v = \mu v$ and $(U T U^*) w = \mu w$ respectively.

Let $E$ be a Hilbert space over a field $\mathbb{k}$, and let $T: E \to E$ be a linear operator. If $T$ is symmetric ($hT$), then for any unitary operator $U$ on $E$, the operator $U T U^*$ (the conjugation of $T$ by $U$) is also symmetric. Here, $U^*$ denotes the adjoint of $U$, represented as `star U.val`.

Let $E$ be a finite-dimensional inner product space over $\mathbb{k}$ and $T: E \to E$ be a symmetric linear operator ($hT$). Given a unitary operator $U$, let $T' = U T U^*$ be the conjugation of $T$ by $U$. There exists a permutation $\sigma \in S_n$ (an element of `Equiv.Perm (Fin n)`) such that the sequence of eigenvalues of $T'$, denoted by $\text{eigenvalues}(U T U^*)$, is equal to the sequence of eigenvalues of $T$ permuted by $\sigma$. In other words, the multiset of eigenvalues of a symmetric operator is invariant under unitary conjugation.