Def UpperHalfPlane.ofComplex

Modification history

2024-10-18 21:29

Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean

chore: Rename `OpenEmbedding` to `IsOpenEmbedding` (#17898) …

Modified UpperHalfPlane.ofComplex View on Github →

2024-05-27 14:30

Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean

Eisenstein series are mdifferentiable (#11013) …

Added UpperHalfPlane.ofComplex View on Github →