smulAux — Mathlib

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)

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