Theorem UpperHalfPlane.gl_smul_I_eq_I_iff_of_neg

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_neg View on Github →