English
For any complex z, tan(2z) = 2 tan z / (1 − tan^2 z), with the usual restriction that both sides are defined (i.e., cos z ≠ 0 and cos 2z ≠ 0).
Русский
Для любого комплексного числа z верно tan(2z) = 2 tan z / (1 − tan^2 z), при условии, что обе стороны определены (то есть cos z ≠ 0 и cos 2z ≠ 0).
LaTeX
$$$$ \tan(2z) = \frac{2 \tan z}{1 - \tan^2 z}. $$$$
Lean4
theorem tan_two_mul {z : ℂ} : tan (2 * z) = (2 : ℂ) * tan z / ((1 : ℂ) - tan z ^ 2) :=
by
by_cases h : ∀ k : ℤ, z ≠ (2 * k + 1) * π / 2
· rw [two_mul, two_mul, sq, tan_add (Or.inl ⟨h, h⟩)]
· rw [not_forall_not] at h
rw [two_mul, two_mul, sq, tan_add (Or.inr ⟨h, h⟩)]