Theorem UpperHalfPlane.σ_conj

Modification history

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