Commit 2025-05-12 23:33 165f83af

View on Github →

refactor(Analysis/Complex/UpperHalfPlane): split off Moebius action (#24824) Split up Mathlib.Analysis.Complex.UpperHalfPlane.Basic into one file which is really basic (just elementary definitions) and another which does the GL(2, R)^+ action.

Estimated changes

deleted theorem ModularGroup.SL_neg_smul
deleted def ModularGroup.coe
deleted def ModularGroup.coeHom
deleted theorem ModularGroup.coeHom_apply
deleted theorem ModularGroup.coe_inj
deleted theorem ModularGroup.coe_one
deleted theorem ModularGroup.denom_S
deleted theorem ModularGroup.denom_apply
deleted theorem ModularGroup.det_coe
deleted theorem ModularGroup.sl_moeb
deleted theorem UpperHalfPlane.coe_smul
deleted theorem UpperHalfPlane.denom_one
deleted theorem UpperHalfPlane.im_smul
deleted theorem UpperHalfPlane.mul_smul'
deleted theorem UpperHalfPlane.neg_smul
deleted def UpperHalfPlane.num
deleted theorem UpperHalfPlane.re_smul
added def ModularGroup.coe
added theorem ModularGroup.coe_inj
added theorem ModularGroup.coe_one
added theorem ModularGroup.denom_S
added theorem ModularGroup.det_coe
added theorem ModularGroup.sl_moeb
added theorem UpperHalfPlane.im_smul
added theorem UpperHalfPlane.re_smul