Commit 2023-07-02 13:59 8dc87f23

View on Github →

feat: port Analysis.Complex.UpperHalfPlane.Manifold (#5658) Also define UpperHalfPlane.coe so that type synonym doesn't leak through API.

Estimated changes

Modified Mathlib.lean

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

deleted theorem UpperHalfPlane.SpecialLinearGroup.im_smul_eq_div_normSq

added theorem UpperHalfPlane.ext'

modified theorem UpperHalfPlane.ext

added theorem UpperHalfPlane.ext_iff

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

added theorem UpperHalfPlane.mdifferentiable_coe

added theorem UpperHalfPlane.smooth_coe

Modified Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean

Modified Mathlib/NumberTheory/Modular.lean

Modified Mathlib/NumberTheory/ModularForms/SlashActions.lean

Modified Mathlib/NumberTheory/ZetaFunction.lean