Helling's theorem: the maximal subgroups of SL₂(ℝ) commensurable with SL₂(ℤ)
Formal statements and proofs, in Lean 4 with Mathlib, of Helling's theorem and of consequences for normalizers. A subgroup G ≤ SL₂(ℝ) is commensurable with SL₂(ℤ) if G ∩ SL₂(ℤ) has finite index in G and in SL₂(ℤ); Γ₀(N)⁺ is the group generated by the Atkin–Lehner elements of level N, and contains Γ₀(N). Every G commensurable with SL₂(ℤ) is conjugate into Γ₀(N)⁺ for some squarefree N, by (det A)^{−1/2}·A for an integral matrix A with det A > 0. For every N ≥ 1, Γ₀(N)⁺ is commensurable with SL₂(ℤ), and for squarefree N it is maximal among such groups; so the maximal subgroups of SL₂(ℝ)…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-22-000033
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-22-000033/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-22-000033/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'