Theorem UpperHalfPlane.norm_ρ

Modification history

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