20.1. Basic definitions🔗

Mathlib contains each of the following definitions:

Complex.sin (z : ℂ) : ℂ#check Complex.sin
Complex.cos (z : ℂ) : ℂ#check Complex.cos
Complex.tan (z : ℂ) : ℂ#check Complex.tan

For Complex.tan, which has poles at ± π / 2, ± 3π / 2, ± 5π / 2, the junk value 0 is used:

open Complex in
example (k : ℤ) :
    tan (π / 2 + k * π) = 0 := byk:ℤ⊢ tan (↑π / 2 + ↑k * ↑π) = 0
  convert tan_int_mul_pi_div_two (2 * k + 1)k:ℤ⊢ ↑π / 2 + ↑k * ↑π = ↑(2 * k + 1) * ↑π / 2
  grindAll goals completed! 🐙

The hyperbolic variants are also available:

Complex.sinh (z : ℂ) : ℂ#check Complex.sinh
Complex.cosh (z : ℂ) : ℂ#check Complex.cosh
Complex.tanh (z : ℂ) : ℂ#check Complex.tanh

In addition, specialised variants over the real numbers exist:

Real.sin (x : ℝ) : ℝ#check Real.sin
Real.cos (x : ℝ) : ℝ#check Real.cos
Real.tan (x : ℝ) : ℝ#check Real.tan

as well as the "inverse" functions over the reals:

Real.arcsin : ℝ → ℝ#check Real.arcsin
Real.arccos (x : ℝ) : ℝ#check Real.arccos
Real.arctan (x : ℝ) : ℝ#check Real.arctan