Commit 2023-06-27 21:00 2f4c17b6

View on Github →

feat: port Analysis.Complex.UpperHalfPlane.Basic (#4335)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean

added theorem UpperHalfPlane.SLOnGLPos_smul_apply

added theorem UpperHalfPlane.SL_neg_smul

added theorem UpperHalfPlane.SpecialLinearGroup.im_smul_eq_div_normSq

added theorem UpperHalfPlane.c_mul_im_sq_le_normSq_denom

added theorem UpperHalfPlane.coe_im

added theorem UpperHalfPlane.coe_mk

added theorem UpperHalfPlane.coe_pos_real_smul

added theorem UpperHalfPlane.coe_re

added theorem UpperHalfPlane.coe_smul

added theorem UpperHalfPlane.coe_vadd

added def UpperHalfPlane.denom

added theorem UpperHalfPlane.denom_apply

added theorem UpperHalfPlane.denom_cocycle

added theorem UpperHalfPlane.denom_ne_zero

added theorem UpperHalfPlane.exists_SL2_smul_eq_of_apply_zero_one_eq_zero

added theorem UpperHalfPlane.exists_SL2_smul_eq_of_apply_zero_one_ne_zero

added theorem UpperHalfPlane.ext

added def UpperHalfPlane.im

added theorem UpperHalfPlane.im_inv_neg_coe_pos

added theorem UpperHalfPlane.im_ne_zero

added theorem UpperHalfPlane.im_pos

added theorem UpperHalfPlane.im_smul

added theorem UpperHalfPlane.im_smul_eq_div_normSq

added theorem UpperHalfPlane.linear_ne_zero

added def UpperHalfPlane.mk

added theorem UpperHalfPlane.mk_coe

added theorem UpperHalfPlane.mk_im

added theorem UpperHalfPlane.mk_re

added theorem UpperHalfPlane.modular_S_smul

added theorem UpperHalfPlane.modular_T_smul

added theorem UpperHalfPlane.modular_T_zpow_smul

added theorem UpperHalfPlane.mul_smul'

added theorem UpperHalfPlane.ne_zero

added theorem UpperHalfPlane.neg_smul

added theorem UpperHalfPlane.normSq_denom_ne_zero

added theorem UpperHalfPlane.normSq_denom_pos

added theorem UpperHalfPlane.normSq_ne_zero

added theorem UpperHalfPlane.normSq_pos

added def UpperHalfPlane.num

added theorem UpperHalfPlane.pos_real_im

added theorem UpperHalfPlane.pos_real_re

added def UpperHalfPlane.re

added theorem UpperHalfPlane.re_add_im

added theorem UpperHalfPlane.re_smul

added theorem UpperHalfPlane.sl_moeb

added def UpperHalfPlane.smulAux'

added theorem UpperHalfPlane.smulAux'_im

added def UpperHalfPlane.smulAux

added theorem UpperHalfPlane.specialLinearGroup_apply

added theorem UpperHalfPlane.subgroup_moeb

added theorem UpperHalfPlane.subgroup_on_SL_apply

added theorem UpperHalfPlane.subgroup_on_glpos_smul_apply

added theorem UpperHalfPlane.subgroup_to_sl_moeb

added theorem UpperHalfPlane.vadd_im

added theorem UpperHalfPlane.vadd_re

added def UpperHalfPlane

Modified Mathlib/Data/Polynomial/Laurent.lean

added theorem LaurentPolynomial.ext

deleted theorem ext

Modified Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup.lean