ThmDex – An index of mathematical definitions, results, and conjectures.
Set of symbols
Alphabet
Deduction system
Theory
Zermelo-Fraenkel set theory
Set
Binary cartesian set product
Binary relation
Map
Cartesian product
Complex cartesian product
Real cartesian product
Euclidean real Cartesian product
Set of complex numbers
Complex number
Definition D507
Complex conjugate
Formulation 1
Let $z = (x, y) \in \mathbb{C}$ be a D1207: Complex number.
The complex conjugate of $z$ is the D1207: Complex number \begin{equation} \overline{z} : = (x, - y) \end{equation}
Results
R5299: Complex conjugate of a binary sum equals sum of complex conjugates
R5297: Complex conjugate of a product of two complex numbers
R2413: Complex conjugate of real number
R4706: Complex conjugate zero iff argument zero