Normalizers of the congruence subgroups Γ_H
Formal statements and proofs, in Lean 4 with Mathlib, about the normalizers in SL₂(ℝ) of every congruence subgroup Γ ⊇ Γ(N), that is, of every Γ_H for H ≤ SL₂(ℤ/N): Nor(Γ)/Γ is finite, of order at most [SL₂(ℤ) : Γ]·Σ_{D ∣ N} ψ(D); the local restrictions of Dose–Lido–Mercuri on the determinants of normalizing matrices; if, at every p ∣ N, H mod p fixes no line or H mod p^{v_p(N)} lies in a split Cartan subgroup, then Nor(Γ_H)/Γ_H ≅ N(H)/H; and at prime level the order is always [N(H) : H], or 2·[N(H) : H] when H fixes exactly one line. 21 theorems, no sorry, only the axioms propext,…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-18-000017
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-18-000017/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-18-000017/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'