Def Mathlib.Meta.Positivity.evalUpperHalfPlaneCoe

Modification history

2025-11-19 06:07
Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
chore: move Mathlib to the module system (#31786) …
Deleted Mathlib.Meta.Positivity.evalUpperHalfPlaneCoeView on Github →
2024-01-24 15:59
Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
feat(UpperHalfPlane): add positivity extensions (#9545)
Added Mathlib.Meta.Positivity.evalUpperHalfPlaneCoeView on Github →