tan_pi_sub

Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

URI: https://scilib.ai/kg/mathlib#Complex.tan_pi_sub

English

For all complex x, tan(π − x) = −tan x.

Русский

Для любого комплексного x tan(π − x) = −tan x.

LaTeX

$$$\tan\bigl(\pi - x\bigr) = -\tan x$$$

Lean4

theorem tan_pi_sub (x : ℂ) : tan (π - x) = -tan x :=
  tan_neg x ▸ tan_periodic.sub_eq'

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

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

Разделы

Аффилиация

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