sin_ne_zero_iff — Mathlib

English

Let θ be a complex number. sin θ ≠ 0 if and only if for all integers k, θ ≠ k π.

Русский

Пусть θ — комплексное число. sin θ ≠ 0 тогда и только тогда, когда для всех целых k выполняется θ ≠ k π.

LaTeX

$$$$\\sin\\theta \\neq 0 \\iff \\forall k \\in \\mathbb{Z}, \\theta \\neq k \\pi$$$$

Lean4

theorem sin_ne_zero_iff {θ : ℂ} : sin θ ≠ 0 ↔ ∀ k : ℤ, θ ≠ k * π := by rw [← not_exists, not_iff_not, sin_eq_zero_iff]

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