im_smul_eq_div_normSq

Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

URI: https://scilib.ai/kg/mathlib#UpperHalfPlane.im_smul_eq_div_normSq

English

The imaginary part of g • z equals |det g| times Im(z) divided by |denom g z|^2.

Русский

Мнимая часть g • z равна |det g| × Im(z) / |denom(g,z)|^2.

LaTeX

$$$\\\\operatorname{Im}(g\\\\cdot z) = \\\\frac{|\\\\det g| \\\\cdot z.im}{\\\\lvert denom(g,z) \\\\rvert^2}$$$

Lean4

theorem im_smul_eq_div_normSq : (g • z).im = |g.det.val| * z.im / Complex.normSq (denom g z) :=
  smulAux'_im g z

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

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

Разделы

Аффилиация

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