tan_two_mul — Mathlib

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⟩)]

Похожие утверждения