tan_two_mul

Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

URI: https://scilib.ai/kg/mathlib#Real.tan_two_mul

English

For any x ∈ ℝ, tan(2x) = 2 tan x / (1 − tan^2 x).

Русский

Для любого x ∈ ℝ верно: tan(2x) = 2 tan x / (1 − tan^2 x).

LaTeX

$$$ \tan(2x) = \frac{2 \tan x}{1 - \tan^2 x}$$$

Lean4

theorem tan_two_mul : tan (2 * x) = 2 * tan x / (1 - tan x ^ 2) :=
  by
  have := @Complex.tan_two_mul x
  norm_cast at *

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru