tan_eq_zero_iff' — Mathlib

English

If cos θ ≠ 0, then tan θ = 0 iff ∃ k ∈ ℤ with θ = kπ.

Русский

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

LaTeX

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

Lean4

theorem tan_eq_zero_iff' {θ : ℝ} (hθ : cos θ ≠ 0) : tan θ = 0 ↔ ∃ k : ℤ, k * π = θ :=
  by
  revert hθ
  exact_mod_cast @Complex.tan_eq_zero_iff' θ

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