Commit 2024-01-24 15:59 4fe00865

View on Github →

feat(UpperHalfPlane): add positivity extensions (#9545)

Estimated changes

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

added def Mathlib.Meta.Positivity.evalUpperHalfPlaneCoe

added def Mathlib.Meta.Positivity.evalUpperHalfPlaneIm

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