tan_periodic

Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

URI: https://scilib.ai/kg/mathlib#Real.Angle.tan_periodic

← MathLib Explorer

English

The tangent function on angles is π-periodic: tan(θ + π) = tan θ.

Русский

Функция тангенса по углам периодическая с периодом π: tan(θ + π) = tan θ.

LaTeX

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

Lean4

theorem tan_periodic : Function.Periodic tan (π : Angle) :=
  by
  intro θ
  induction θ using Real.Angle.induction_on
  rw [← coe_add, tan_coe, tan_coe]
  exact Real.tan_periodic _

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

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

Разделы

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

Аффилиация

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