English
Let x,y be complex numbers satisfying the standard pole-avoidance condition for tan with imaginary shifts (the tangent of x and of i y avoids odd multiples of π/2). Then tan(x + i y) = (tan x + i tanh y) / (1 − i tan x tanh y).
Русский
Пусть x,y ∈ ℂ удовлетворяют условию избегания полюсов тангенса в сочетании с мнимой частью (tan x и i y избегают нечётных кратных π/2). Тогда 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_add_mul_I {x y : ℂ}
(h :
((∀ k : ℤ, x ≠ (2 * k + 1) * π / 2) ∧ ∀ l : ℤ, y * I ≠ (2 * l + 1) * π / 2) ∨
(∃ k : ℤ, x = (2 * k + 1) * π / 2) ∧ ∃ l : ℤ, y * I = (2 * l + 1) * π / 2) :
tan (x + y * I) = (tan x + tanh y * I) / (1 - tan x * tanh y * I) := by rw [tan_add h, tan_mul_I, mul_assoc]
