Complex conjugate of a complex number

Set

 @#55CCEE: context
 postulate $\mathrm{conj}:X\to \mathbb C$
 $a+i\ b\in X$ $a,b\in \mathbb R$
 postulate $\mathrm{conj}(a+i\ b):= a-i\ b$

Ramifications

If $z\in \mathbb C$, one writes $\overline z\equiv\mathrm{conj}(z)$.