Let $z_1, \dots, z_N \in \mathbb{C}$ each be a D1207: Complex number.
Then
\begin{equation}
\overline{\sum_{n = 1}^N z_n}
= \sum_{n = 1}^N \overline{z_n}
\end{equation}
▶ | R5299: Complex conjugate of a binary sum equals sum of complex conjugates |