{"id":"palomar/PALOMAR-2026-10-18-000017","url":"https://github.com/F-Najman/normalizer-lean/tree/e7ca694d9e349326e03e5acfa4e41ed823e4e2dc","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-18-000017-v2.json","repo":"https://github.com/F-Najman/normalizer-lean","tags":["math.NT","math.GR","msc:11F06","msc:20H05","msc:14G35","msc:14H37","msc:68V20","modular-forms","congruence-subgroups","lean"],"score":0,"title":"Normalizers of the congruence subgroups Γ_H","trust":"high","domain":"math.NT","source":"palomar","authors":["Filip Najman"],"reviews":0,"subject":"math.NT","summary":"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,…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-20","reactions":{},"formalized":true,"formalizes":[{"title":"Automorphisms of general modular curves","identifier":"arXiv:2610.08998v1","relationship":"formalizes"}]}