Theorem UpperHalfPlane.eq_of_re_of_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.eq_of_re_of_normView on Github →