Complex trigonometric functions #
Basic facts and derivatives for the complex trigonometric functions.
theorem
Complex.tendsto_abs_tan_of_cos_eq_zero
{x : ℂ}
(hx : cos x = 0)
:
Filter.Tendsto (fun (x : ℂ) => abs (tan x)) (nhdsWithin x {x}ᶜ) Filter.atTop
@[simp]