arctan_neg

Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

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

English

arctan(-x) = -arctan x for all real x.

Русский

arctan(-x) = -arctan x для всех x ∈ ℝ.

LaTeX

$$$\\arctan(-x) = -\\arctan x$$$

Lean4

@[simp]
theorem arctan_neg (x : ℝ) : arctan (-x) = -arctan x := by simp [arctan_eq_arcsin, neg_div]

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

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

Разделы

Аффилиация

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