div_re — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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