sin_eq_zero_iff_cos_eq — Mathlib

English

For any complex z, sin z = 0 if and only if cos z = 1 or cos z = -1.

Русский

Для любого комплексного z верно: sin z = 0 тогда и только тогда, когда cos z = 1 или cos z = -1.

LaTeX

$$$$\sin z = 0 \iff \cos z = 1 \lor \cos z = -1.$$$$

Lean4

theorem sin_eq_zero_iff_cos_eq {z : ℂ} : sin z = 0 ↔ cos z = 1 ∨ cos z = -1 := by
  rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, right_eq_add, mul_eq_zero, or_self]

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