The normalizer of Γ_Δ(N) for every N and every Δ
Formal statements and proofs, in Lean 4 with Mathlib, about the normalizer in SL₂(ℝ) of Γ_Δ(N) for every N ≥ 1 and every subgroup Δ ≤ (ℤ/N)ˣ, with or without −1. Let h* be the largest h with h² ∣ N, d² ≡ 1 (mod h) for every d ∈ Δ, and Δ ⊇ ker((ℤ/N)ˣ → (ℤ/(N/h))ˣ); let n* = N/h*² and D* = diag(h*, 1). Then D*⁻¹Γ₀(n*)D* ≤ Nor(Γ_Δ(N)) ≤ D*⁻¹Γ₀(n*)⁺D*; an Atkin–Lehner element w_Q of level n* (conjugated by D*) normalizes Γ_Δ(N) iff ι*_Q(Δ̄) = Δ̄, where ι*_Q inverts the components of (ℤ/(N/h*))ˣ at the primes of Q; so Nor(Γ_Δ(N)) is described exactly, its index over Γ_Δ(N) is [(ℤ/N)ˣ :…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-20-000007
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-20-000007/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-20-000007/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'