English
smulAux defines the action of GL(2,R) on the upper half-plane: z ↦ smulAux(g,z) ∈ ℍ, given by smulAux'(g,z) as the complex coordinate and a positive imaginary part.
Русский
smulAux задаёт действие GL(2, ℝ) на верхней полуплоскости: z ↦ smulAux(g,z) ∈ ℍ, где smulAux'(g,z) задаёт комплексную координату, а мнимая часть положительна.
LaTeX
$$$smulAux(g,z) = \\left( smulAux'(g,z), \\frac{|\\\\det g| \\\\operatorname{Im}(z)}{|\\\\operatorname{denom}(g,z)|^{2}} \\right)$$$
Lean4
/-- Fractional linear transformation, also known as the Moebius transformation -/
def smulAux (g : GL (Fin 2) ℝ) (z : ℍ) : ℍ :=
mk (smulAux' g z) <| by
rw [smulAux'_im]
exact div_pos (mul_pos (abs_pos.mpr g.det.ne_zero) z.im_pos) (normSq_denom_pos _ z.im_ne_zero)