Commit 2022-06-03 07:58 2b69bb43

View on Github →

feat(analysis/complex/upper_half_plane): extend action on upper half plane to GL_pos (#12415) This extends the action on the upper half plane from SL_2 to GL_pos,

Estimated changes

Modified src/analysis/complex/upper_half_plane.lean

added theorem upper_half_plane.SL_neg_smul

added theorem upper_half_plane.SL_on_GL_pos_smul_apply

modified theorem upper_half_plane.coe_smul

modified def upper_half_plane.denom

added theorem upper_half_plane.denom_apply

modified theorem upper_half_plane.denom_cocycle

modified theorem upper_half_plane.denom_ne_zero

modified theorem upper_half_plane.im_smul

modified theorem upper_half_plane.im_smul_eq_div_norm_sq

modified theorem upper_half_plane.mul_smul'

modified theorem upper_half_plane.neg_smul

modified theorem upper_half_plane.norm_sq_denom_ne_zero

modified theorem upper_half_plane.norm_sq_denom_pos

modified def upper_half_plane.num

modified theorem upper_half_plane.re_smul

added theorem upper_half_plane.sl_moeb

modified def upper_half_plane.smul_aux'

modified theorem upper_half_plane.smul_aux'_im

modified def upper_half_plane.smul_aux

added theorem upper_half_plane.special_linear_group.im_smul_eq_div_norm_sq

added theorem upper_half_plane.subgroup_moeb

added theorem upper_half_plane.subgroup_on_GL_pos_smul_apply

added theorem upper_half_plane.subgroup_on_SL_apply

added theorem upper_half_plane.subgroup_to_sl_moeb

Modified src/number_theory/modular.lean

modified theorem modular_group.coe_T_zpow_smul_eq

deleted theorem modular_group.coe_smul

deleted theorem modular_group.denom_apply

deleted theorem modular_group.im_smul

deleted theorem modular_group.im_smul_eq_div_norm_sq

deleted theorem modular_group.neg_smul

deleted theorem modular_group.re_smul

deleted theorem modular_group.smul_coe