sin_eq_sin_iff — Mathlib

English

For complex x and y, 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_sin_iff {x y : ℂ} : sin x = sin y ↔ ∃ k : ℤ, y = 2 * k * π + x ∨ y = (2 * k + 1) * π - x :=
  by
  simp only [← Complex.cos_sub_pi_div_two, cos_eq_cos_iff, sub_eq_iff_eq_add]
  refine exists_congr fun k => or_congr ?_ ?_ <;> refine Eq.congr rfl ?_ <;> simp [field] <;> ring

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