re_eq_add_conj — Mathlib

English

For any z ∈ ℂ, the real part satisfies Re(z) = (z + conj(z))/2.

Русский

Для любого z ∈ ℂ вещественная часть удовлетворяет Re(z) = (z + conj(z))/2.

LaTeX

$$$\\operatorname{Re}(z) = \\dfrac{z + \\overline{z}}{2}$$$

Lean4

/-- A complex number `z` plus its conjugate `conj z` is `2` times its real part. -/
theorem re_eq_add_conj (z : ℂ) : (z.re : ℂ) = (z + conj z) / 2 := by
  simp only [add_conj, ofReal_mul, ofReal_ofNat, mul_div_cancel_left₀ (z.re : ℂ) two_ne_zero]

Похожие утверждения