two_mul_arctan_add_pi

Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

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

← MathLib Explorer

English

If x > 1, then 2 arctan x = arctan(2x/(1−x^2)) + π.

Русский

Если x > 1, то 2 arctan x = arctan(2x/(1−x^2)) + π.

LaTeX

$$$x > 1 \\Rightarrow 2 \\arctan x = \\arctan\\\\left(\\\\frac{2x}{1-x^2}\\\\right) + π.$$$

Lean4

theorem two_mul_arctan_add_pi (h : 1 < x) : 2 * arctan x = arctan (2 * x / (1 - x ^ 2)) + π := by
  rw [two_mul, arctan_add_eq_add_pi (by nlinarith) (by linarith)]; congr 2; ring

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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