sin_eq_zero_iff — Mathlib

English

Let x and y be complex numbers. sin x = sin y if and only if there exists an integer k such that y = 2kπ + x or y = (2k+1)π - x.

Русский

Пусть x и y — комплексные числа. sin x = sin y тогда и только тогда, когда существует целое k такое, что y = 2kπ + x или y = (2k+1)π − x.

LaTeX

$$$$\\sin x = \\sin y \\iff \\exists k \\in \\mathbb{Z}, \\ y = 2k\\pi + x \\lor \\ y = (2k+1)\\pi - x$$$$

Lean4

theorem sin_eq_zero_iff {θ : ℂ} : sin θ = 0 ↔ ∃ k : ℤ, θ = k * π :=
  by
  rw [← Complex.cos_sub_pi_div_two, cos_eq_zero_iff]
  constructor
  · rintro ⟨k, hk⟩
    use k + 1
    simp [eq_add_of_sub_eq hk]
    ring
  · rintro ⟨k, rfl⟩
    use k - 1
    simp
    ring

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