sin_eq_one_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem sin_eq_one_iff {x : ℂ} : sin x = 1 ↔ ∃ k : ℤ, π / 2 + k * (2 * π) = x :=
  by
  rw [← cos_sub_pi_div_two, cos_eq_one_iff]
  simp only [eq_sub_iff_add_eq']

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