im_eq_sub_conj — Mathlib

English

For any z ∈ ℂ, the imaginary part satisfies Im(z) = (z - conj(z))/(2i).

Русский

Для любого z ∈ ℂ мнимая часть удовлетворяет Im(z) = (z - conj(z))/(2i).

LaTeX

$$$\\operatorname{Im}(z) = \\dfrac{z - \\overline{z}}{2i}$$$

Lean4

/-- A complex number `z` minus its conjugate `conj z` is `2i` times its imaginary part. -/
theorem im_eq_sub_conj (z : ℂ) : (z.im : ℂ) = (z - conj z) / (2 * I) := by
  simp only [sub_conj, ofReal_mul, ofReal_ofNat, mul_right_comm,
    mul_div_cancel_left₀ _ (mul_ne_zero two_ne_zero I_ne_zero : 2 * I ≠ 0)]

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