Theorem UpperHalfPlane.sigma_J

Modification history

2025-07-03 03:52
Mathlib/NumberTheory/ModularForms/Basic.lean
feat(NumberTheory/ModularForms): GL(2, R) action preserves holomorphy (#25894) …
Added UpperHalfPlane.sigma_JView on Github →