two_mul_arctan_inv_2_sub_arctan_inv_7

Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

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

← MathLib Explorer

English

2 arctan(1/2) − arctan(1/7) = π/4.

Русский

2 arctan(1/2) − arctan(1/7) = π/4.

LaTeX

$$$2 \\\\arctan(\\\\frac{1}{2}) - \\\\arctan(\\\\frac{1}{7}) = \\\\frac{\\\\pi}{4}.$$$

Lean4

theorem two_mul_arctan_inv_2_sub_arctan_inv_7 : 2 * arctan 2⁻¹ - arctan 7⁻¹ = π / 4 := by
  rw [two_mul_arctan, ← arctan_one, sub_eq_iff_eq_add, arctan_add] <;> norm_num

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

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

Разделы

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

Аффилиация

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