QuantumInfo.ForMathlib.IsMaximalSelfAdjoint

Let $R$ be a commutative semiring with a star operation $*$ ($R$ is a `CommSemiring` and has a `Star` instance). If the star operation is trivial, meaning $x^* = x$ for all $x \in R$ (an instance of `TrivialStar`), then $R$ is its own maximal self-adjoint subalgebra. Under this condition, the map from the ring of scalars to the self-adjoint elements is the identity map, and the self-adjoint parts of the algebra coincide with the ring $R$ itself.

Let $\alpha$ be an $\mathbb{R}$-clike field (a field such as $\mathbb{R}$ or $\mathbb{C}$ equipped with a conjugation). The type of real numbers $\mathbb{R}$ is the maximal self-adjoint sub-algebra of $\alpha$. Specifically, the map from an element of $\alpha$ to its self-adjoint part is given by the real part $\text{Re}: \alpha \to \mathbb{R}$, and an element $x \in \alpha$ is self-adjoint (i.e., $\bar{x} = x$) if and only if $x = \text{Re}(x)$.

Let $R$ be a commutative semiring equipped with a star operation. If the star operation is trivial (i.e., $x^* = x$ for all $x \in R$), then the map $\text{selfadjMap} : R \to R$, which maps an element to its self-adjoint part, is equal to the identity map $\text{id}_R$.

Let $\alpha$ be a field that is $\mathbb{R}$-clike (such as $\mathbb{R}$ or $\mathbb{C}$). The map $\text{selfadjMap}: \alpha \to \mathbb{R}$, which sends an element to its self-adjoint part, is equal to the real part function $\text{Re}$.