Def UpperHalfPlane.σ

Modification history

2025-09-16 15:34

Mathlib/Analysis/Complex/UpperHalfPlane/MoebiusAction.lean

feat(NumberTheory/ModularForms): define boundedness / vanishing at a cusp (#29560)

Deleted UpperHalfPlane.σ View on Github →

2025-05-19 12:23

Mathlib/Analysis/Complex/UpperHalfPlane/MoebiusAction.lean

feat(Analysis/UpperHalfPlane, ModularForms): extend actions from GLPos to GL (#24830) …

Added UpperHalfPlane.σ View on Github →