QuantumInfo.ForMathlib.HermitianMat.Basic

Let $n$ be a type (representing the set of indices) and $\alpha$ be a type equipped with an additive group structure and a star-addition monoid structure (providing a notion of involution or conjugation). The type `HermitianMat n α` is the subtype of $n \times n$ matrices over $\alpha$ that are Hermitian. A matrix $M \in \text{Matrix}_n(\alpha)$ belongs to this type if it is equal to its adjoint, i.e., $M = M^*$, where $M^*$ is the conjugate transpose of $M$ (the translation of the `selfAdjoint` property to the matrix algebra).

Let \( n \) be a type and \( \alpha \) be a type with a star-addition monoid structure. The function maps a Hermitian matrix \( A \) of type `HermitianMat n α` to its underlying \( n \times n \) matrix representation in `Matrix n n α`. This is achieved by taking the value of the subtype.

Let \( n \) be a type and \( \alpha \) be a type equipped with an addition group structure and a star-addition monoid structure. There exists a coercion from the type of Hermitian matrices `HermitianMat n α` to the type of \( n \times n \) matrices `Matrix n n α`. This coercion is defined by mapping a Hermitian matrix \( A \) to its underlying matrix representation \( \text{mat}(A) \).

For any Hermitian matrix $A$ of size $n \times n$ with entries in $\alpha$, the underlying matrix value associated with the structure $A$, denoted by $A.val$, is equal to the matrix obtained by applying the coercion from Hermitian matrices to general square matrices, $A$.

Let $A = \langle x, h \rangle$ be a Hermitian matrix constructed from an $n \times n$ matrix $x$ and a proof $h$ that $x$ is Hermitian. Then the underlying matrix representation of $A$, denoted as $\text{mat}(A)$, is equal to $x$.

Let $A$ be a Hermitian matrix in $\text{HermitianMat}(n, \alpha)$ and $h$ be a proof that its underlying matrix $A.\text{mat}$ satisfies the predicate $\text{IsHermitian}$. Then the new Hermitian matrix constructed from the pair $\langle A.\text{mat}, h \rangle$ is equal to the original Hermitian matrix $A$.

Let $A$ be a Hermitian matrix in $\text{HermitianMat}(n, \alpha)$. Then the underlying matrix of $A$, denoted as $A.\text{mat}$, satisfies the property $\text{IsHermitian}$.

Let $A$ and $B$ be Hermitian matrices of size $n \times n$ with entries in $\alpha$. If the underlying matrices of $A$ and $B$ are equal (i.e., $A.\text{mat} = B.\text{mat}$), then $A$ and $B$ are equal as Hermitian matrices.

Let $\text{HermitianMat}(n, \alpha)$ be the type of Hermitian matrices of size $n \times n$ with entries in $\alpha$. The structure `HermitianMat.instFun` defines a coercion such that an element $M$ of $\text{HermitianMat}(n, \alpha)$ can be treated as a function (or a matrix) mapping indices $(i, j) \in n \times n$ to their corresponding entry $M_{ij} \in \alpha$. This coercion is injective, meaning that if two Hermitian matrices have the same entries for all indices, they are equal.

Let $A$ be a Hermitian matrix of size $n \times n$ with entries in $\alpha$, and let $A.\text{mat}$ denote its underlying matrix representation. For any indices $i, j \in n$, the entry in the $i$-th row and $j$-th column of the underlying matrix, denoted by $A.\text{mat}_{i,j}$, is equal to the value of the Hermitian matrix viewed as a function evaluated at $i$ and $j$, denoted by $A(i, j)$.

Let $A$ be a Hermitian matrix of size $n \times n$ over a type $\alpha$ that admits an additive group structure and a star additive monoid structure. Let $A.\text{mat}$ denote the underlying matrix of $A$. Then the conjugate transpose of $A.\text{mat}$ is equal to itself, i.e., $(A.\text{mat})^\text{H} = A.\text{mat}$.

For a given type $n$ and a type $\alpha$ equipped with an additive group structure and a star additive monoid structure (providing a conjugate transpose operation), the set of Hermitian matrices $\text{HermitianMat}(n, \alpha)$—defined as matrices $A \in M_n(\alpha)$ such that $A^\dagger = A$—forms an additive group under matrix addition.

If the index set $n$ is empty, then the type of Hermitian matrices $\text{HermitianMat}(n, \alpha)$—where $\alpha$ is an additive group with a star operation—possesses a unique element. This element is defined to be the zero matrix, and every Hermitian matrix in this space is equal to it.

For a given type $n$ and a star additive monoid $\alpha$ with an additive group structure, the underlying matrix of the zero Hermitian matrix $0 \in \text{HermitianMat}(n, \alpha)$ is the zero matrix $0 \in M_n(\alpha)$.

Given a type $n$ and a ring $\alpha$ with a star operation, let $0$ be the zero matrix in the space of $n \times n$ matrices over $\alpha$. If $h$ is a proof that this zero matrix is Hermitian (i.e., $0 = 0^\dagger$), then the Hermitian matrix constructed from the zero matrix and the proof $h$ is equal to the zero element of the type of Hermitian matrices $\text{HermitianMat}(n, \alpha)$.

For any indices $i, j$ of type $n$, the $(i, j)$-th entry of the zero Hermitian matrix $0 \in \text{HermitianMat}(n, \mathbb{k})$ is equal to zero.

For any two Hermitian matrices $A$ and $B$, the matrix representation of their sum is equal to the sum of their individual matrix representations, that is $(A + B).\text{mat} = A.\text{mat} + B.\text{mat}$.

For any two Hermitian matrices $A$ and $B$ (of type `HermitianMat n α`), the matrix representation of their difference is equal to the difference of their individual matrix representations, i.e., $(A - B).\text{mat} = A.\text{mat} - B.\text{mat}$.

For any Hermitian matrix $A$, the matrix associated with the additive inverse $-A$ is equal to the additive inverse of the matrix associated with $A$, denoted as $(-A)_{\text{mat}} = - (A_{\text{mat}})$.

Given a ring $R$ and the type of $n \times n$ Hermitian matrices over $\alpha$ (denoted $\text{HermitianMat}_n(\alpha)$), we define a scalar multiplication operation $\cdot: R \times \text{HermitianMat}_n(\alpha) \to \text{HermitianMat}_n(\alpha)$. For a scalar $c \in R$ and a Hermitian matrix $A$, the resulting matrix $c \cdot A$ is obtained by multiplying the underlying matrix $A_{\text{mat}}$ by $c$. The definition ensures that the resulting matrix remains Hermitian (self-adjoint).

Let $R$ be a scalar ring, $n$ be an index type, and $\alpha$ be a type with an addition group and a star-addition monoid structure. For any scalar $c \in R$ and any Hermitian matrix $A \in \text{HermitianMat}(n, \alpha)$, the matrix representation of the scalar product $c \cdot A$ is equal to the scalar product of $c$ and the matrix representation of $A$, i.e., $(c \cdot A)_{\text{mat}} = c \cdot (A_{\text{mat}})$.

Let $R$ be a scalar ring, $n$ be an index type, and $\alpha$ be a type with an addition group and a star-addition monoid structure. For any scalar $c \in R$, any Hermitian matrix $A \in \text{HermitianMat}(n, \alpha)$, and any indices $i, j \in n$, the entry at position $(i, j)$ of the scalar product $c \cdot A$ is equal to the scalar product of $c$ and the $(i, j)$-th entry of $A$. That is, $(c \cdot A)_{ij} = c \cdot A_{ij}$.

Let $n$ be an index type and $\alpha$ be a type with an additive group structure and a star addition monoid structure. The space $\text{HermitianMat}(n, \alpha)$ of Hermitian matrices (defined as matrices $A$ such that $A = A^\dagger$) is equipped with a topological space structure. This topology is the one induced by viewing $\text{HermitianMat}(n, \alpha)$ as the set of self-adjoint elements of the matrix algebra $M_n(\alpha)$.

Let $n$ be an index type and $\alpha$ be a type with an additive group structure and a star addition monoid structure. Let $\text{HermitianMat}(n, \alpha)$ denote the space of Hermitian matrices with entries in $\alpha$, and let $M_n(\alpha)$ denote the space of $n \times n$ matrices over $\alpha$. The map $\text{mat} : \text{HermitianMat}(n, \alpha) \to M_n(\alpha)$, which sends a Hermitian matrix to its underlying matrix, is continuous.

Let $X$ be a topological space and $s \subseteq X$ be a subset. For any function $f: X \to \text{HermitianMat}(n, \alpha)$ mapping into the space of Hermitian matrices, $f$ is continuous on $s$ if and only if the composition map $x \mapsto (f(x)).\text{mat}$ (the underlying matrix-valued function) is continuous on $s$. Here, $\text{HermitianMat}(n, \alpha)$ denotes the set of matrices $A \in \text{Mat}(n, n, \alpha)$ such that $A^\dagger = A$.

The addition operation on the space of Hermitian matrices $\text{HermitianMat}(n, \alpha)$ is continuous with respect to its topological structure.

In the space of Hermitian matrices of size $n$ with entries in $\alpha$, the negation operation $A \mapsto -A$ is continuous. Here, `HermitianMat n α` denotes the type of matrices $A$ such that $A^\dagger = A$, equipped with its natural topological space structure.

For any type $n$ and any type $\alpha$ that is an additive group and a star additive monoid, the additive group of Hermitian matrices $\text{HermitianMat}(n, \alpha)$—equipped with its natural topological structure—is a topological additive group. This means that both the addition operation $(A, B) \mapsto A + B$ and the negation operation $A \mapsto -A$ are continuous.

Let $n$ be a type and $\alpha$ be a topological ring with a continuous involution (star-monoid). The space of Hermitian matrices of size $n$ over $\alpha$, denoted as $\text{HermitianMat } n \ \alpha$, possesses a continuous scalar multiplication by a topological ring $R$. Specifically, the map $(r, A) \mapsto r \cdot A$ is continuous for $r \in R$ and $A \in \text{HermitianMat } n \ \alpha$.

For any type $n$, let $\mathbb{k}$ be a field equipped with a topological structure such that it forms a topological additive group with a continuous involution. The additive group of Hermitian matrices over $\mathbb{k}$ of size $n$, denoted $\text{HermitianMat}(n, \mathbb{k})$, is a topological additive group. This implies that the addition operation $(A, B) \mapsto A + B$ and the negation operation $A \mapsto -A$ are continuous on the space of Hermitian matrices.

Let $n$ be a type and $\mathbb{C}$ be the field of complex numbers. The space of Hermitian matrices of size $n$ over $\mathbb{C}$, denoted as $\text{HermitianMat } n \ \mathbb{C}$, has a continuous scalar multiplication by the field of real numbers $\mathbb{R}$. That is, the map $(r, A) \mapsto r \cdot A$ from $\mathbb{R} \times \text{HermitianMat } n \ \mathbb{C}$ to $\text{HermitianMat } n \ \mathbb{C}$ is continuous.

Let $n$ be a type representing the indices and $\mathbb{k}$ be a field (typically $\mathbb{R}$ or $\mathbb{C}$). The space of Hermitian matrices $\text{HermitianMat}(n, \mathbb{k})$ is a $T_3$ space, meaning it is a Hausdorff space ($T_1$) that is also regular.

Given a ring $R$, a type $n$ representing indices, and a type $\alpha$ equipped with addition and a star-operation (typically the complex numbers $\mathbb{C}$), the type of Hermitian matrices $\text{HermitianMat}(n, \alpha)$ possesses a multiplication action (scalar action) by $R$. This action is defined such that for any $r \in R$ and any Hermitian matrix $H$, the result $r \cdot H$ is determined by the scalar multiplication of the underlying matrix, ensuring the action is compatible with the inclusion of Hermitian matrices into the space of all matrices.

For a given set of indices $n$ and a type $\alpha$ that forms an additive commutative group with a star-operation, the type of Hermitian matrices $\text{HermitianMat}(n, \alpha)$ forms an additive commutative group. This structure is inherited from the underlying space of $n \times n$ matrices over $\alpha$, as Hermitian matrices form an additive subgroup.

Let $n$ and $\alpha$ be types such that $\alpha$ is an additive commutative group with a star operation. For any finite set $s$ and any collection of Hermitian matrices $f_i$ indexed by $i \in s$, the matrix representation of the sum of these Hermitian matrices is equal to the sum of their individual matrix representations: $$\left( \sum_{i \in s} f_i \right).\text{mat} = \sum_{i \in s} (f_i.\text{mat})$$ where `.mat` denotes the underlying $n \times n$ matrix of a Hermitian matrix.

Let $n$ and $\alpha$ be types such that $\alpha$ is a ring with a star operation, and let $R$ be a scalar ring. The type of Hermitian matrices $\text{HermitianMat}(n, \alpha)$—defined as the set of self-adjoint matrices $A$ such that $A^* = A$—forms a module over $R$. This structure is inherited from the module property of self-adjoint elements within the space of $n \times n$ matrices over $\alpha$.

Let $n$ be an index type and $\alpha$ be a type with the structure of a topological star-module over a ring $R$. The function maps a Hermitian matrix $H \in \text{HermitianMat}(n, \alpha)$ to its underlying matrix in $\text{Matrix}(n, n, \alpha)$. This map is defined as a continuous linear map over $R$, denoted as: $$\text{mat}_L : \text{HermitianMat}(n, \alpha) \to L_R(\text{Matrix}(n, n, \alpha))$$ where the linearity follows from the additive and scaling properties of the underlying matrix representation, and continuity is derived from the topological structure of the Hermitian space.

An instance of the identity element for the type of Hermitian matrices. It defines $1 \in \text{HermitianMat}_n(\alpha)$ as the identity matrix $I$, provided that $I$ satisfies the condition of being a Hermitian matrix (i.e., $I^* = I$).

The matrix representation of the identity element in the space of Hermitian matrices $\text{HermitianMat}(n, \alpha)$ is equal to the identity matrix $I \in \text{Matrix}(n, n, \alpha)$. Here, $n$ is the index type and $\alpha$ is a type with addition and a star-operation (typically $\mathbb{C}$ or $\mathbb{R}$).

Let $n$ be an index type and $\alpha$ be a type with addition and a star operation (specifically an additive group with a star monoid structure). Given that the identity matrix $1 \in \text{Matrix}_{n \times n}(\alpha)$ satisfies the property $(1 : \text{Matrix}_{n \times n}(\alpha)).\text{IsHermitian}$, then constructing a Hermitian matrix from this identity matrix yields the identity element of the Hermitian matrix type, denoted as $(1 : \text{HermitianMat}_n(\alpha))$.

Let $n$ be an index type and $\alpha$ be a type with an additive group and star-monoid structure. For any indices $i, j \in n$, the $(i, j)$-th entry of the identity Hermitian matrix $1 \in \text{HermitianMat}_n(\alpha)$ is equal to the $(i, j)$-th entry of the identity matrix $I \in \text{Matrix}_{n \times n}(\alpha)$.

For an index type $n$ and a field (or ring with star operation) $\mathbb{k}$, the set of Hermitian matrices $\text{HermitianMat}_n(\mathbb{k})$ forms an additive commutative monoid with a multiplicative identity $1$. This structure includes a commutative addition operation, a zero element $0$, and a specific element $1$ corresponding to the identity matrix $I$, satisfying the standard axioms for an additive commutative monoid with one.

Let $n$ be a nonempty type and $\mathbb{k}$ be a ring. Let $\text{HermitianMat}(n, \mathbb{k})$ denote the type of Hermitian matrices with indices in $n$ and entries in $\mathbb{k}$. The identity Hermitian matrix $1$ is not equal to the zero Hermitian matrix $0$.

Let $\text{HermitianMat}(m, \alpha)$ denote the type of Hermitian matrices with indices in $m$ and entries in $\alpha$. The inversion operator $A \mapsto A^{-1}$ on $\text{HermitianMat}(m, \alpha)$ is defined such that the inverse of a Hermitian matrix $A$ is the Hermitian matrix whose underlying matrix is the matrix inverse $A^{-1}$.

Let $A$ be a Hermitian matrix of type `HermitianMat m α`. The matrix representation of the inverse of the Hermitian matrix $A$ is equal to the inverse of the matrix representation of $A$. That is, $(A^{-1})_{\text{mat}} = (A_{\text{mat}})^{-1}$.

Let $0$ be the zero Hermitian matrix of size $m \times m$ with entries in $\alpha$. The inverse of this zero Hermitian matrix is equal to the zero Hermitian matrix, i.e., $0^{-1} = 0$.

Let $1$ be the identity Hermitian matrix of type $\text{HermitianMat}(m, \alpha)$. The inverse of this identity Hermitian matrix is equal to the identity Hermitian matrix, i.e., $1^{-1} = 1$.

The power operation for Hermitian matrices defines the $n$-th power of a Hermitian matrix $A \in \text{HermitianMat}_m(\alpha)$ for any natural number $n \in \mathbb{N}$. The resulting matrix $A^n$ is also Hermitian, satisfying the condition $(A^n)^\dagger = A^n$ where $\dagger$ denotes the conjugate transpose.

Let $A$ be a Hermitian matrix. For any natural number $n$, the matrix representation of the $n$-th power of $A$ is equal to the $n$-th power of the matrix representation of $A$, denoted as $(A^n)_{\text{mat}} = (A_{\text{mat}})^n$.

For any Hermitian matrix $A$, its zeroth power is the identity matrix, denoted as $A^0 = I$. Here, $I$ represents the identity element of the space of Hermitian matrices.

For any non-zero natural number $n$, the $n$-th power of the zero Hermitian matrix $0 \in \text{HermitianMat}_m(\alpha)$ is equal to zero, i.e., $0^n = 0$. Here, $\alpha$ is a type with addition and a star operation (specifically an `AddGroup` and `StarAddMonoid`), and $m$ is the index type of the matrix.

Let $I$ be the identity element in the space of Hermitian matrices $\text{HermitianMat}_m(\alpha)$. For any natural number $n$, the $n$-th power of $I$ is equal to $I$, i.e., $1^n = 1$.

The definition provides an instance of the power operator for Hermitian matrices raised to an integer exponent. For a Hermitian matrix $A \in \text{HermitianMat}_m(\alpha)$ and an integer $z \in \mathbb{Z}$, the power $A^z$ is defined by taking the $z$-th power of the underlying matrix (i.e., $(A_{\text{mat}})^z$) and verifying that the resulting matrix remains Hermitian. Here, $\alpha$ is a type with addition and a star operation, and $m$ is the index type of the matrix.

Let $A$ be a Hermitian matrix of size $n \times n$ with entries in a type $\alpha$ that satisfies the properties of an additive group and a star-addition monoid. For any integer $z \in \mathbb{Z}$, the matrix underlying the $z$-th power of the Hermitian matrix $A$ is equal to the $z$-th power of the matrix underlying $A$. That is, $(A^z)_{\text{mat}} = (A_{\text{mat}})^z$.

Let $A$ be a Hermitian matrix. For any natural number $n \in \mathbb{N}$, the integer power of $A$ by $n$ (cast as an integer) is equal to the natural power of $A$ by $n$. That is, $A^{(n : \mathbb{Z})} = A^n$.

Let $A$ be a Hermitian matrix of size $n \times n$ with entries in a type $\alpha$ that satisfies the properties of an additive group and a star-addition monoid. Then $A$ raised to the integer power of $0$ is equal to the identity Hermitian matrix $I$, i.e., $A^{(0 : \mathbb{Z})} = 1$.

Let $A$ be a Hermitian matrix. Then $A$ raised to the integer power of $1$ is equal to $A$, i.e., $A^{(1 : \mathbb{Z})} = A$.

Let $I$ be the identity matrix in the space of Hermitian matrices of size $m$ over a ring/field $\alpha$ with a star-addition monoid structure. For any integer $z \in \mathbb{Z}$, the integer power of the identity Hermitian matrix $I^z$ is equal to $I$.

Let $A$ be a Hermitian matrix. Then $A$ raised to the integer power of $-1$ is equal to its inverse, i.e., $A^{-1} = A^{(-1 : \mathbb{Z})}$. Here, the left-hand side denotes the integer power operation and the right-hand side denotes the matrix inversion operator.

Let $A$ be a Hermitian matrix of size $m \times m$ over a type $\alpha$ that supports inversion and integer powers. For any integer $z \in \mathbb{Z}$, the integer power of the inverse of $A$, denoted $(A^{-1})^z$, is equal to the inverse of the $z$-th power of $A$, denoted $(A^z)^{-1}$.

Let $\alpha$ be a commutative ring and $A$ be a square matrix over $\alpha$. The inverse of the matrix $A$, denoted $A^{-1}$, commutes with $A$ itself, such that $A^{-1} A = A A^{-1}$.

Let $A$ be a Hermitian matrix. The matrix representation of the inverse of $A$ commutes with the matrix representation of $A$, such that $A^{-1}_{\text{mat}} A_{\text{mat}} = A_{\text{mat}} A^{-1}_{\text{mat}}$.

Let $A$ be a Hermitian matrix. Then $A$ commutes with its inverse, specifically in terms of their underlying matrix representations, i.e., $A \cdot A^{-1} = A^{-1} \cdot A$.

Let $n$ be a finite type and $\mathbb{K}$ be an `RCLike` field (such as $\mathbb{R}$ or $\mathbb{C}$). The space of Hermitian matrices $\text{HermitianMat}(n, \mathbb{K})$, consisting of matrices $A$ such that $A^* = A$, is a finite-dimensional vector space over the real numbers $\mathbb{R}$.

Let $A$ be a Hermitian matrix with entries in a field $\mathbb{K}$ (where $\mathbb{K}$ is $\mathbb{R}$ or $\mathbb{C}$, or more generally an `RCLike` field). For any index $x$, the imaginary part of the diagonal element $A_{xx}$ is zero; that is, $\text{im}(A_{xx}) = 0$.

Let $A$ be a Hermitian matrix with complex entries indexed by $n$. For any index $x \in n$, the imaginary part of the diagonal element $A_{xx}$ is zero: $\text{Im}(A_{xx}) = 0$.

Let $\alpha$ be a ring with a star operation (conjugate transpose). For any (possibly rectangular) matrix $B \in M_{m \times n}(\alpha)$, the function $\text{conj}_B$ is an additive group homomorphism from the set of $n \times n$ Hermitian matrices to the set of $m \times m$ Hermitian matrices. For any Hermitian matrix $A \in \text{HermitianMat}(n, \alpha)$, the map is defined by the congruence transformation $A \mapsto B A B^\dagger$, where $B^\dagger$ denotes the conjugate transpose of $B$.

Let $A$ be a Hermitian matrix of size $n \times n$ with entries in $\alpha$, and let $B$ be an $m \times n$ matrix. The congruence transformation of $A$ by $B$, denoted by $\text{conj}(B, A)$, is the Hermitian matrix whose underlying matrix is given by the product $B A B^\dagger$, where $B^\dagger$ is the conjugate transpose of $B$. Formally, $\text{conj}(B, A) = \langle B \cdot A_{\text{mat}} \cdot B^\dagger, P \rangle$, where $A_{\text{mat}}$ is the matrix representation of $A$ and $P$ is the proof that the resulting matrix is Hermitian.

Let $A$ be a Hermitian matrix of size $n \times n$ and $B$ be a matrix of size $m \times n$ with entries in a ring support star operations. The matrix representation of the congruence transformation of $A$ by $B$, denoted as $A\text{.conj } B$, is equal to the matrix product $B A B^*$, where $A^* = B^\text{H}$ is the conjugate transpose of $B$.

Let $A$ be a Hermitian matrix of size $n \times n$. Let $B$ be an $m \times n$ matrix and $C$ be an $l \times m$ matrix, where $m$ is a finite index type. The composition of two congruence transformations applied to $A$ satisfies $(A_{\text{conj } B})_{\text{conj } C} = A_{\text{conj } (CB)}$. That is, first transforming $A$ by $B$ and then transforming the result by $C$ is equivalent to transforming $A$ by the product matrix $CB$.

Let $A$ be a Hermitian matrix of size $n \times n$ with entries in an additive group $\alpha$ equipped with a star operation. For any $m$, let $0_{m \times n}$ be the zero matrix of size $m \times n$. The congruence transformation of $A$ by the zero matrix, denoted as $\text{conj}(0_{m \times n}, A)$, is equal to the zero Hermitian matrix of size $m \times m$.

Let $A$ be a Hermitian matrix of size $n \times n$ with entries in $\alpha$, where $n$ is a type with decidable equality. Let $I$ denote the $n \times n$ identity matrix. The congruence transformation of $A$ by the identity matrix, denoted as $\text{conj}(I, A)$, is equal to $A$. In terms of matrix multiplication, this corresponds to the identity $I A I^\dagger = A$.

Let $n$ be a finite type with decidable equality and $\alpha$ be a ring with a star operation. For any unitary matrix $U$ in the unitary group $U(n, \alpha)$, the congruence transformation of the identity Hermitian matrix $1$ by $U$ is equal to the identity Hermitian matrix $1$. That is, $\text{conj}(U, 1) = 1$, which corresponds to the matrix identity $U I U^* = I$.

Let $R$ be a ring of scalars, and let $n$ and $m$ be index types. For a given $m \times n$ matrix $B$ over a star-ring $\alpha$, the map $\text{conj}_B : \text{HermitianMat}(n, \alpha) \to \text{HermitianMat}(m, \alpha)$ defined by $A \mapsto B A B^*$ is an $R$-linear map. Here, $B^*$ denotes the conjugate transpose of $B$.

Let $A$ be a Hermitian matrix of size $n \times n$ over a ring $\alpha$, and let $B$ be an $m \times n$ matrix. The evaluation of the linear map $\text{conjLinear}_R(B)$ at $A$ is equal to the congruent transformation $\text{conj}_B(A)$, which is defined as $B A B^*$, where $B^*$ denotes the conjugate transpose of $B$.