English
Under the same pole-avoidance framework as above, tan(x + i y) equals (tan x + i tanh y) / (1 − i tan x tanh y).
Русский
При том же условии избегания полюсов тангенса, tan(x + i y) равно (tan x + i tanh y) / (1 − i tan x tanh y).
LaTeX
$$$$ \tan(x + i y) = \frac{\tan x + i \tanh y}{1 - i \tan x \tanh y}. $$$$
Lean4
theorem tan_eq {z : ℂ}
(h :
((∀ k : ℤ, (z.re : ℂ) ≠ (2 * k + 1) * π / 2) ∧ ∀ l : ℤ, (z.im : ℂ) * I ≠ (2 * l + 1) * π / 2) ∨
(∃ k : ℤ, (z.re : ℂ) = (2 * k + 1) * π / 2) ∧ ∃ l : ℤ, (z.im : ℂ) * I = (2 * l + 1) * π / 2) :
tan z = (tan z.re + tanh z.im * I) / (1 - tan z.re * tanh z.im * I) := by convert tan_add_mul_I h;
exact (re_add_im z).symm