div_re — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem div_re (z w : K) : re (z / w) = re z * re w / normSq w + im z * im w / normSq w := by
  simp only [div_eq_mul_inv, mul_assoc, sub_eq_add_neg, neg_mul, mul_neg, neg_neg, rclike_simps]

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