Theorem UpperHalfPlane.pos_real_smul_injective

Modification history

2026-02-04 15:37
Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
chore(UpperHalfPlane): redefine as a structure (#34597) …
Added UpperHalfPlane.pos_real_smul_injectiveView on Github →