ThmDex – An index of mathematical definitions, results, and conjectures.
Complex conjugate of a complex eigenvalue of a real matrix is an eigenvalue
Formulation 0
Let $A \in \mathbb{R}^{N \times N}$ be a D4571: Real matrix such that
(i) $\lambda \in \mathbb{C}$ is a D1207: Complex number
(ii) $z \in \mathbb{C}^{N \times 1} \setminus \{ \boldsymbol{0} \}$ is a D5689: Complex column matrix
(iii) \begin{equation} A z = \lambda z \end{equation}
Then \begin{equation} A \overline{z} = \overline{\lambda} \overline{z} \end{equation}
Proofs
Proof 0
Let $A \in \mathbb{R}^{N \times N}$ be a D4571: Real matrix such that
(i) $\lambda \in \mathbb{C}$ is a D1207: Complex number
(ii) $z \in \mathbb{C}^{N \times 1} \setminus \{ \boldsymbol{0} \}$ is a D5689: Complex column matrix
(iii) \begin{equation} A z = \lambda z \end{equation}
The matrix complex conjugate $\overline{A}$ is defined pointwise. Hence, this result follows from the results
(i) R5292: Complex conjugate of a complex eigenvalue of a complex matrix is an eigenvalue for the conjugate matrix
(ii) R2413: Complex conjugate of real number

$\square$