tan_eq — Mathlib

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

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