fdo — Mathlib

English

fdo is the open fundamental domain for the SL(2,ℤ) action on the upper half-plane: { z : ℍ | 1 < |z|^2 and |Re z| < 1/2 }.

Русский

fdo есть открытый фундаментальный домен действия SL(2,ℤ) на ℍ: { z ∈ ℍ | 1 < |z|^2 и |Re z| < 1/2 }.

LaTeX

$$$\\mathrm{fdo} = \\{ z \\in \\mathbb{H} : 1 < \\|z\\|^2 \\ \\wedge\\ \\lvert \\Re z \\rvert < \\tfrac{1}{2} \\}.$$$

Lean4

/-- The standard open fundamental domain of the action of `SL(2,ℤ)` on `ℍ`. -/
def fdo : Set ℍ :=
  {z | 1 < normSq (z : ℂ) ∧ |z.re| < (1 : ℝ) / 2}

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