Skip to content

Commit 6726709

Browse files
Parcly-TaxelParcly-Taxel
committed
feat: port Analysis.Complex.UpperHalfPlane.Metric (#5544)
1 parent 5e1c9d6 commit 6726709

File tree

2 files changed

+401
-0
lines changed

2 files changed

+401
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -559,6 +559,7 @@ import Mathlib.Analysis.Complex.Schwarz
559559
import Mathlib.Analysis.Complex.UnitDisc.Basic
560560
import Mathlib.Analysis.Complex.UpperHalfPlane.Basic
561561
import Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
562+
import Mathlib.Analysis.Complex.UpperHalfPlane.Metric
562563
import Mathlib.Analysis.Complex.UpperHalfPlane.Topology
563564
import Mathlib.Analysis.ConstantSpeed
564565
import Mathlib.Analysis.Convex.Basic

0 commit comments

Comments
 (0)