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