Theorem UpperHalfPlane.denom_J

Modification history

2026-03-06 17:09
Mathlib/Analysis/Complex/UpperHalfPlane/MoebiusAction.lean
feat(Analysis/Complex/UpperHalfPlane): invariant measure (#34402) …
Modified UpperHalfPlane.denom_JView on Github →
2025-09-22 11:27
Mathlib/NumberTheory/ModularForms/Basic.lean
feat(NumberTheory/ModularForms): tweak def of slash-action (#29804) …
Modified UpperHalfPlane.denom_JView 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_JView on Github →