cos_nat_mul_two_pi_add_pi

Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

← MathLib Explorer

English

For all n ∈ ℕ, cos((n·2π) + π) = -1.

Русский

Для любого n ∈ ℕ косинус((n·2π) + π) равен −1.

LaTeX

$$$\forall n \in \mathbb{N},\ \cos\left(n\cdot 2\pi + \pi\right) = -1$$$

Lean4

theorem cos_nat_mul_two_pi_add_pi (n : ℕ) : cos (n * (2 * π) + π) = -1 := by
  simpa only [cos_zero] using (cos_periodic.nat_mul n).add_antiperiod_eq cos_antiperiodic

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

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

Разделы

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

Аффилиация

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