cos_eq_one_iff — Mathlib

English

For complex x, cos x = 1 if and only if there exists an integer k with x = 2 k π.

Русский

Для комплексного x: cos x = 1 тогда и только тогда, когда существует целое k такое, что x = 2kπ.

LaTeX

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

Lean4

theorem cos_eq_one_iff {x : ℂ} : cos x = 1 ↔ ∃ k : ℤ, k * (2 * π) = x :=
  by
  rw [← cos_zero, eq_comm, cos_eq_cos_iff]
  simp [mul_assoc, mul_left_comm, eq_comm]

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