smulAux'_im — Mathlib

English

Same as the previous item: Im(smulAux'(g,z)) = |det g| · Im(z) / |denom g z|^2.

Русский

То же самое: Im(smulAux'(g,z)) = |det g| · Im(z) / |denom(g,z)|^2.

LaTeX

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

Lean4

theorem smulAux'_im (g : GL (Fin 2) ℝ) (z : ℂ) : (smulAux' g z).im = |g.det.val| * z.im / Complex.normSq (denom g z) :=
  by
  simp only [smulAux', σ]
  split_ifs with h <;> [rw [abs_of_pos h]; rw [abs_of_nonpos (not_lt.mp h)]] <;>
    simpa only [starRingAut_apply, Complex.star_def, Complex.conj_im, neg_mul, neg_div, neg_inj] using moebius_im g z

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