div_im — Mathlib

English

For any z,w ∈ K, the imaginary part of z/w equals (Im z Re w − Re z Im w) / ||w||^2.

Русский

Для любых z,w ∈ K мнимая часть z/w равна (Im z Re w − Re z Im w) / ||w||^2.

LaTeX

$$$$ \operatorname{Im}\left(\frac{z}{w}\right) = \frac{\operatorname{Im}(z) \operatorname{Re}(w) - \operatorname{Re}(z) \operatorname{Im}(w)}{\|w\|^2}. $$$$

Lean4

theorem div_im (z w : K) : im (z / w) = im z * re w / normSq w - re z * im w / normSq w := by
  simp only [div_eq_mul_inv, mul_assoc, sub_eq_add_neg, add_comm, neg_mul, mul_neg, rclike_simps]
    -- Not `@[simp]` since `simp` can prove this

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