fd — Mathlib · SciLib

English

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

Русский

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

LaTeX

$$$\\mathrm{fd} = \\{ z \\in \\mathbb{H} : 1 \\le \\|z\\|^2 \\text{ и } |\\Re z| \\le \\tfrac{1}{2} \\}.$$$

Lean4

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

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