linear maps $p,q$ are equal if and only if $\langle p x, x \rangle = \langle q x, x \rangle$ for any $x$.

copy of linear_map.ext_iff_inner_map but for continuous linear maps

Self-adjoint linear operators $p,q$ are equal if and only if $\langle p x, x \rangle_\mathbb{k} = \langle q x, x \rangle_\mathbb{k}$.

in a complex inner product space, we have that an operator $a$ is self-adjoint if and only if $\langle a x, x \rangle_\mathbb{C}$ is real for all $x \in E$

the adjoint of a self-adjoint operator is self-adjoint

for a self-adjoint operator $a$, we have $\langle a x, x \rangle_\mathbb{k}$ is real

copy of inner_map_self_eq_zero for bounded linear maps