im_smul_eq_div_normSq — Mathlib

English

If g ∈ SL(2, ℤ) and z ∈ ℍ with g represented as (a b; c d), then the imaginary part transforms as Im(g•z) = Im(z) / |c z + d|^2.

Русский

Если g представлена матрицей (a b; c d) ∈ SL(2, ℤ) и z ∈ ℍ, то Im(g•z) = Im(z) / |c z + d|^2.

LaTeX

$$$\Im(g \cdot z) = \dfrac{\Im(z)}{|c z + d|^2}$, \quad g = \begin{pmatrix} a & b \\ c & d \end{pmatrix}$$$

Lean4

theorem im_smul_eq_div_normSq : (g • z).im = z.im / Complex.normSq (denom g z) := by
  simpa using z.im_smul_eq_div_normSq g

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