im_eq_conj_sub — Mathlib

English

Im z equals I times (conj z − z) / 2 in the embedding.

Русский

Мнимая часть z равна I(конъугированное z минус z) делённое на 2, через вложение.

LaTeX

$$$\uparrow(\operatorname{Im} z) = \dfrac{I \bigl( \operatorname{conj}(z) - z \bigr)}{2}$$$

Lean4

theorem im_eq_conj_sub (z : K) : ↑(im z) = I * (conj z - z) / 2 := by
  rw [← neg_inj, ← ofReal_neg, ← I_mul_re, re_eq_add_conj, map_mul, conj_I, ← neg_div, ← mul_neg, neg_sub, mul_sub,
    neg_mul, sub_eq_add_neg]

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