Theorem UpperHalfPlane.petersson_slash_SL

Modification history

2025-09-23 06:31
Mathlib/NumberTheory/ModularForms/Petersson.lean
feat(NumberTheory/ModularForms): integrand for Petersson product (#29640) …
Added UpperHalfPlane.petersson_slash_SLView on Github →