moebius_im — Mathlib

English

For any g,h ∈ GL(2,ℝ) and z ∈ ℂ, σ g (num h z) = num h (σ g z) and σ g (denom h z) = denom h (σ g z).

Русский

Для любых g,h ∈ GL(2,ℝ) и z ∈ ℂ выполняется σ g (num h z) = num h (σ g z) и σ g (denom h z) = denom h (σ g z).

LaTeX

$$$$ \\sigma(g)(\\mathrm{num}(h,z)) = \\mathrm{num}(h, \\sigma(g)(z)), \\quad \\sigma(g)(\\mathrm{denom}(h,z)) = \\mathrm{denom}(h, \\sigma(g)(z)). $$$$

Lean4

theorem moebius_im (g : GL (Fin 2) ℝ) (z : ℂ) :
    (num g z / denom g z).im = g.det.val * z.im / Complex.normSq (denom g z) :=
  by
  simp only [num, denom, Complex.div_im, Complex.add_im, Complex.mul_im, Complex.ofReal_re, Complex.ofReal_im, zero_mul,
    add_zero, Complex.add_re, Complex.mul_re, sub_zero, ← sub_div, GeneralLinearGroup.val_det_apply, g.1.det_fin_two]
  ring

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