Commit 2023-12-26 12:09 351b5cc4

View on Github →

feat: Positivity extensions for Real.sinh, Real.cosh (#9098) Also fix the name of Real.Mathlib.Meta.Positivity.evalExp to Mathlib.Meta.Positivity.evalRealPi.

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean

added def Mathlib.Meta.Positivity.evalRealPi

deleted def Real.Mathlib.Meta.Positivity.evalExp

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean

added def Mathlib.Meta.Positivity.evalSinh

added theorem Real.sinh_eq_zero

added theorem Real.sinh_ne_zero

Modified Mathlib/Data/Complex/Exponential.lean

added def Mathlib.Meta.Positivity.evalCosh