Difference_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 \Im z$ be the imaginary part of $z$ . Then $z - \overline z = 2 i \, \map \Im z$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Difference_of_Complex_Number_with_Conjugate (z : ℂ) : z - starRingEnd ℂ z = 2 * z.im * Complex.I := by sorry

Source

https://proofwiki.org/wiki/Difference_of_Complex_Number_with_Conjugate

View graph