Theorem UpperHalfPlane.gl_smul_I_eq_I_iff_of_pos

Modification history

2026-05-13 03:36

Mathlib/Analysis/Complex/UpperHalfPlane/FixedPoints.lean

feat(UpperHalfPlane): define PGL action on the upper half-plane (#36330)

Added UpperHalfPlane.gl_smul_I_eq_I_iff_of_pos View on Github →