two_mul_arctan_inv_3_add_arctan_inv_7

Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

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

English

2 arctan(1/3) + arctan(1/7) = π/4.

Русский

2 arctan(1/3) + arctan(1/7) = π/4.

LaTeX

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

Lean4

theorem two_mul_arctan_inv_3_add_arctan_inv_7 : 2 * arctan 3⁻¹ + arctan 7⁻¹ = π / 4 := by
  rw [two_mul_arctan, arctan_add] <;> norm_num

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

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

Разделы

Аффилиация

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