tan_periodic

Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

English

The tangent function is periodic with period π: tan(x + π) = tan x for all x.

Русский

Тангенс имеет период π: tan(x + π) = tan x для всех x.

LaTeX

$$$\tan(x + \pi) = \tan x$$$

Lean4

theorem tan_periodic : Function.Periodic tan π := by
  simpa only [tan_eq_sin_div_cos] using sin_antiperiodic.div cos_antiperiodic

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

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

Разделы

Аффилиация

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