tan_eq_zero_iff' — Mathlib

English

If cos θ ≠ 0, then tan θ = 0 iff θ = k π for some integer k.

Русский

Если cos θ ≠ 0, то tan θ = 0 тогда и только тогда, когда θ = k π для некоторого целого k.

LaTeX

$$$$\\tan\\theta = 0 \\iff \\exists k \\in \\mathbb{Z}, \\theta = k \\pi$$$$

Lean4

/-- If the tangent of a complex number is well-defined,
then it is equal to zero iff the number is equal to `k * π` for an integer `k`.

See also `Complex.tan_eq_zero_iff` for a version that takes into account junk values of `θ`. -/
theorem tan_eq_zero_iff' {θ : ℂ} (hθ : cos θ ≠ 0) : tan θ = 0 ↔ ∃ k : ℤ, k * π = θ := by
  simp only [tan, hθ, div_eq_zero_iff, sin_eq_zero_iff]; simp [eq_comm]

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