English
Let θ be a complex number. tan θ = 0 if and only if there exists an integer k such that k π / 2 = θ.
Русский
Пусть θ — комплексное число. tan θ = 0 тогда и только тогда, существует целое k, такое что θ = k π / 2.
LaTeX
$$$$\\tan\\theta = 0 \\iff \\exists k \\in \\mathbb{Z}, \\theta = k \\frac{\\pi}{2}$$$$
Lean4
/-- The tangent of a complex number is equal to zero
iff this number is equal to `k * π / 2` for an integer `k`.
Note that this lemma takes into account that we use zero as the junk value for division by zero.
See also `Complex.tan_eq_zero_iff'`. -/
theorem tan_eq_zero_iff {θ : ℂ} : tan θ = 0 ↔ ∃ k : ℤ, k * π / 2 = θ :=
by
rw [tan, div_eq_zero_iff, ← mul_eq_zero, ← mul_right_inj' two_ne_zero, mul_zero, ← mul_assoc, ← sin_two_mul,
sin_eq_zero_iff]
simp [field, mul_comm, eq_comm]
