inv_im

Mathlib.Data.Complex.Basic

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

English

For z ∈ ℂ, the imaginary part of the inverse is Im(z⁻¹) = −Im(z) / normSq(z).

Русский

Для z ∈ ℂ мнимая часть обратного равна −Im(z) / normSq(z).

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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