English
For g ∈ GL(2,R) and z ∈ ℍ, the imaginary part of g • z equals the absolute value of the imaginary part of num g z divided by denom g z.
Русский
Для g ∈ GL(2,ℝ) и z ∈ ℍ, Im(g • z) = |Im(num(g,z)/denom(g,z))|.
LaTeX
$$$\\\\operatorname{Im}(g\\\\cdot z) = \\\\left|\\\\frac{ Im( num(g,z) / denom(g,z) ) }\\\\right|$$
Lean4
theorem im_smul : (g • z).im = |(num g z / denom g z).im| :=
by
change (smulAux' g z).im = _
simp only [smulAux', σ, DFunLike.ite_apply, RingHom.id_apply, apply_ite, moebius_im, Complex.conj_im, ← neg_div,
← neg_mul, abs_div, abs_mul, abs_of_pos (show 0 < (z : ℂ).im from z.coe_im ▸ z.im_pos),
abs_of_nonneg <| Complex.normSq_nonneg _]
split_ifs with h <;> [rw [abs_of_pos h]; rw [abs_of_nonpos (not_lt.mp h)]]