Complex_Number_equals_Conjugate_iff_Wholly_Real

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$ . Then $z = \overline z$ $z$ is wholly real.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Complex_Number_equals_Conjugate_iff_Wholly_Real (z : ℂ) : z = starRingEnd ℂ z ↔ z.im = 0 := by sorry

Source