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