inv_re

Mathlib.Data.Complex.Basic

URI: https://scilib.ai/kg/mathlib#Complex.inv_re

English

For z ∈ ℂ, the real part of the inverse is Re(z⁻¹) = Re(z) / normSq(z).

Русский

Для z ∈ ℂ действительная часть обратного равна Re(z) / normSq(z).

LaTeX

$$$$\Re(z^{-1}) = \frac{\Re(z)}{normSq(z)}.$$$$

Lean4

@[simp]
theorem inv_re (z : ℂ) : z⁻¹.re = z.re / normSq z := by simp [inv_def, division_def, ofReal]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru