20.2. Basic properties🔗

Mathlib knows the various relationships between the trigonometric functions and the exponential. For example:

open Complex in
example (z : ℂ) :
    cos z = (exp (z * I) + exp (-z * I)) / 2 :=
  rfl

We note in passing that Mathlib also contains a more general definition of exponential NormedSpace.exp which allows more general scalars, but the trigonometric functions are only defined for the reals and complexes.

Mathlib also knows about the relevant periodicity. For example:

open Complex in
example (z : ℂ) :
    sin (z + 2 * π) = sin z :=
  sin_add_two_pi z

Finally Mathlib knows that these are analytic functions:

open Complex in
example (z : ℂ) :
    AnalyticAt ℂ sin z :=
  analyticAt_sin

and facts about their derivatives such as:

open Complex in
example (z : ℂ) :
    deriv sin = cos :=
  deriv_sin