Theorem UpperHalfPlane.ρ_sq

Modification history

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