Theorem UpperHalfPlane.denom_J

Modification history

2025-09-22 11:27

Mathlib/NumberTheory/ModularForms/Basic.lean

feat(NumberTheory/ModularForms): tweak def of slash-action (#29804) …

Modified UpperHalfPlane.denom_J View on Github →

2025-07-03 03:52

Mathlib/NumberTheory/ModularForms/Basic.lean

feat(NumberTheory/ModularForms): GL(2, R) action preserves holomorphy (#25894) …

Added UpperHalfPlane.denom_J View on Github →