inv_re — Mathlib

English

For any z ∈ K, the real part of z⁻¹ equals the real part of z divided by the squared norm: Re(z⁻¹) = Re(z) / ||z||^2.

Русский

Для любого z ∈ K действительная часть z⁻¹ равна действительной части z делённой на квадрат нормы: Re(z⁻¹) = Re(z) / ||z||^2.

LaTeX

$$$$ \operatorname{Re}(z^{-1}) = \frac{\operatorname{Re}(z)}{\|z\|^2}. $$$$

Lean4

@[simp, rclike_simps]
theorem inv_re (z : K) : re z⁻¹ = re z / normSq z := by
  rw [inv_def, normSq_eq_def', mul_comm, re_ofReal_mul, conj_re, div_eq_inv_mul]

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