cos_eq_neg_one_iff

Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

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

English

cos x = -1 iff there exists k ∈ ℤ with x = π + 2kπ.

Русский

cos x = -1 тогда и только тогда, когда x = π + 2kπ для некоторого k ∈ ℤ.

LaTeX

$$$$ \cos x = -1 \iff \exists k \in \mathbb{Z},\ x = \pi + 2k\pi. $$$$

Lean4

theorem cos_eq_neg_one_iff {x : ℝ} : cos x = -1 ↔ ∃ k : ℤ, π + k * (2 * π) = x :=
  mod_cast @Complex.cos_eq_neg_one_iff x

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

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

Разделы

Аффилиация

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