Trigonometric and hyperbolic trigonometric functions #
This file contains the definitions of the sine, cosine, tangent, hyperbolic sine, hyperbolic cosine, and hyperbolic tangent functions.
The complex sine function, defined via exp
Equations
Instances For
The complex cosine function, defined via exp
Instances For
The complex hyperbolic sine function, defined via exp
Instances For
The complex hyperbolic cosine function, defined via exp
Instances For
The real sine function, defined as the real part of the complex sine
Equations
Instances For
The real cosine function, defined as the real part of the complex cosine
Equations
Instances For
The real tangent function, defined as the real part of the complex tangent
Equations
Instances For
The real hypebolic sine function, defined as the real part of the complex hyperbolic sine
Instances For
The real hypebolic cosine function, defined as the real part of the complex hyperbolic cosine
Instances For
The real hypebolic tangent function, defined as the real part of the complex hyperbolic tangent
Instances For
Extension for the positivity
tactic: Real.cosh
is always positive.