callensxavier/socrateai-fricke-involution

Fricke Involution on Γ₀(N) — Lean 4 Formalization Machine-checked Lean 4 formalization of the Fricke involution WN=(0−1N0)W_N = \begin{pmatrix} 0 & -1 \\ N & 0 \end{pmatrix}WN​=(0N​−10​) on the congruence subgroup Γ₀(N), and of the operator it induces on modular forms — together with the papers written around it and the record of a prior-art audit that changed what those papers claim. DOI: 10.5281/zenodo.22542571 · Author: Xavier Callens · Code: SocrateAI-Lean-Lib (release… See the full description on the dataset page: https://huggingface.co/datasets/callensxavier/socrateai-fricke-involution.