Theorem UpperHalfPlane.ofComplex_apply

Modification history

2024-05-27 14:30
Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean
Eisenstein series are mdifferentiable (#11013) …
Added UpperHalfPlane.ofComplex_applyView on Github →