mathlib documentation

analysis.special_functions.trigonometric.complex

Complex trigonometric functions #

Basic facts and derivatives for the complex trigonometric functions.

theorem complex.cos_eq_zero_iff {θ : } :
complex.cos θ = 0 ∃ (k : ), θ = (2 * k + 1) * π / 2
theorem complex.cos_ne_zero_iff {θ : } :
complex.cos θ 0 ∀ (k : ), θ (2 * k + 1) * π / 2
theorem complex.sin_eq_zero_iff {θ : } :
complex.sin θ = 0 ∃ (k : ), θ = (k) * π
theorem complex.sin_ne_zero_iff {θ : } :
complex.sin θ 0 ∀ (k : ), θ (k) * π
theorem complex.tan_eq_zero_iff {θ : } :
complex.tan θ = 0 ∃ (k : ), θ = (k) * π / 2
theorem complex.tan_ne_zero_iff {θ : } :
complex.tan θ 0 ∀ (k : ), θ (k) * π / 2
theorem complex.cos_eq_cos_iff {x y : } :
complex.cos x = complex.cos y ∃ (k : ), y = (2 * k) * π + x y = (2 * k) * π - x
theorem complex.sin_eq_sin_iff {x y : } :
complex.sin x = complex.sin y ∃ (k : ), y = (2 * k) * π + x y = (2 * k + 1) * π - x
theorem complex.tan_add {x y : } (h : ((∀ (k : ), x (2 * k + 1) * π / 2) ∀ (l : ), y (2 * l + 1) * π / 2) (∃ (k : ), x = (2 * k + 1) * π / 2) ∃ (l : ), y = (2 * l + 1) * π / 2) :
theorem complex.tan_add' {x y : } (h : (∀ (k : ), x (2 * k + 1) * π / 2) ∀ (l : ), y (2 * l + 1) * π / 2) :
theorem complex.tan_two_mul {z : } :
complex.tan (2 * z) = 2 * complex.tan z / (1 - complex.tan z ^ 2)
theorem complex.tan_add_mul_I {x y : } (h : ((∀ (k : ), x (2 * k + 1) * π / 2) ∀ (l : ), y * complex.I (2 * l + 1) * π / 2) (∃ (k : ), x = (2 * k + 1) * π / 2) ∃ (l : ), y * complex.I = (2 * l + 1) * π / 2) :
theorem complex.tan_eq {z : } (h : ((∀ (k : ), (z.re) (2 * k + 1) * π / 2) ∀ (l : ), ((z.im)) * complex.I (2 * l + 1) * π / 2) (∃ (k : ), (z.re) = (2 * k + 1) * π / 2) ∃ (l : ), ((z.im)) * complex.I = (2 * l + 1) * π / 2) :
@[simp]
theorem complex.deriv_tan (x : ) :
theorem real.cos_eq_zero_iff {θ : } :
real.cos θ = 0 ∃ (k : ), θ = (2 * k + 1) * π / 2
theorem real.cos_ne_zero_iff {θ : } :
real.cos θ 0 ∀ (k : ), θ (2 * k + 1) * π / 2
theorem real.cos_eq_cos_iff {x y : } :
real.cos x = real.cos y ∃ (k : ), y = (2 * k) * π + x y = (2 * k) * π - x
theorem real.sin_eq_sin_iff {x y : } :
real.sin x = real.sin y ∃ (k : ), y = (2 * k) * π + x y = (2 * k + 1) * π - x