div_im — Mathlib

English

For z,w ∈ ℂ with w ≠ 0, the imaginary part of z/w is Im(z/w) = (Im(z) Re(w) − Re(z) Im(w)) / |w|^2.

Русский

Для z,w ∈ ℂ с w ≠ 0, мнимая часть z/w равна (Im(z) Re(w) − Re(z) Im(w)) / |w|^2.

LaTeX

$$$$\Im\left(\frac{z}{w}\right) = \frac{\Im(z) \Re(w) - \Re(z) \Im(w)}{normSq(w)}.$$$$

Lean4

theorem div_im (z w : ℂ) : (z / w).im = z.im * w.re / normSq w - z.re * w.im / normSq w := by
  simp [div_eq_mul_inv, mul_assoc, sub_eq_add_neg, add_comm]

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