Def UpperHalfPlane.ρ

Modification history

2026-04-06 13:17
Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
feat(NumberTheory/Modular): strengthen 2nd Fundamental-Domain Lemma (#36736) …
Added UpperHalfPlane.ρView on Github →