tan_add' — Mathlib

English

For complex x and y satisfying the same non-undefined conditions, tan(x+y) equals (tan x + tan y) / (1 − tan x tan y).

Русский

Для комплексных x и y при условии, что тангенсы определены, tan(x+y) равно (tan x + tan y) / (1 − tan x tan y).

LaTeX

$$$$\\tan(x+y) = \\frac{\\tan x + \\tan y}{1 - \\tan x \\tan y}$$$$

Lean4

theorem tan_add' {x y : ℂ} (h : (∀ k : ℤ, x ≠ (2 * k + 1) * π / 2) ∧ ∀ l : ℤ, y ≠ (2 * l + 1) * π / 2) :
    tan (x + y) = (tan x + tan y) / (1 - tan x * tan y) :=
  tan_add (Or.inl h)

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