abs_det — Mathlib

English

Same as 150877: there exists γ ∈ SL(2,ℤ) with 1/2 ≤ im(γ•τ).

Русский

То же, что и в 150877: существует γ ∈ SL(2,ℤ) такое, что 1/2 ≤ im(γ•τ).

LaTeX

$$$\forall \tau \in \mathbb{H}, \exists \gamma\in SL(2,\mathbb{Z}), \tfrac{1}{2} \le \operatorname{im}(\gamma\cdot \tau)$$$

Lean4

theorem abs_det [LinearOrder R] [IsOrderedRing R] [HasDetPlusMinusOne Γ] {g} (hg : g ∈ Γ) : |g.det.val| = 1 := by
  rcases HasDetPlusMinusOne.det_eq hg with h | h <;> simp [h]

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