Mathlib v3 is deprecated. Go to Mathlib v4

Theorem upper_half_plane.subgroup_on_GL_pos_smul_apply

Modification history

2022-06-03 07:58

src/analysis/complex/upper_half_plane.lean

feat(analysis/complex/upper_half_plane): extend action on upper half plane to GL_pos (#12415) …

Added upper_half_plane.subgroup_on_GL_pos_smul_apply View on Github →