coe_specialLinearGroup_apply — Mathlib

English

For g ∈ SL(2,R) and z ∈ ℍ, the complex coordinate of g • z equals ((a z + b)/(c z + d)) with a,b,c,d the entries of g, after mapping Re to ℂ.

Русский

Для g ∈ SL(2,ℝ) и z ∈ ℍ вещественные коэффициенты матрицы преобразуются в комплексный коэффициент: g•z = (a z + b)/(c z + d).

LaTeX

$$$↑(g \\cdot z) = \\frac{(a z + b)}{(c z + d)} \\quad \\text{where } g = \\begin{pmatrix}a&b\\\\ c&d\\end{pmatrix}$$$

Lean4

theorem coe_specialLinearGroup_apply {R : Type*} [CommRing R] [Algebra R ℝ] (g : SL(2, R)) (z : ℍ) :
    ↑(g • z) =
      (((algebraMap R ℝ (g 0 0) : ℂ) * z + (algebraMap R ℝ (g 0 1) : ℂ)) /
        ((algebraMap R ℝ (g 1 0) : ℂ) * z + (algebraMap R ℝ (g 1 1) : ℂ))) :=
  by
  rw [MulAction.compHom_smul_def, coe_smul_of_det_pos (by simp)]
  rfl

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