Sum_of_Complex_Number_with_Conjugate

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

complex-conjugatesproofwiki

Let $z \in \C$ be a complex number. Let $\overline z$ be the complex conjugate of $z$ . Let $\map \Re z$ be the real part of $z$ . Then $z + \overline z = 2 \, \map \Re z$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Sum_of_Complex_Number_with_Conjugate (z : ℂ) : z + starRingEnd ℂ z = 2 * ↑z.re := by sorry

Source

https://proofwiki.org/wiki/Sum_of_Complex_Number_with_Conjugate

View graph