Commit 2025-08-23 19:57 5a9a6887

View on Github →

feat(Trigonometric/Deriv): add IsEquivalent lemmas (#28810) Add sin ~[𝓝 0] id, sinh ~[𝓝 0] id for real and complex numbers.

Estimated changes

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

added theorem Complex.isEquivalent_sin

added theorem Complex.isEquivalent_sinh

added theorem Real.isEquivalent_sin

added theorem Real.isEquivalent_sinh