Def Mathlib.Meta.Positivity.evalCosh

Modification history

2023-12-26 12:09

Mathlib/Data/Complex/Exponential.lean

feat: Positivity extensions for `Real.sinh`, `Real.cosh` (#9098) …

Added Mathlib.Meta.Positivity.evalCosh View on Github →