tan_ne_zero_iff

Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

URI: https://scilib.ai/kg/mathlib#Real.tan_ne_zero_iff

English

tan θ ≠ 0 iff θ ≠ kπ/2 for all integers k.

Русский

tan θ ≠ 0 если и только если для всех целых k θ ≠ kπ/2.

LaTeX

$$$$ \tan \theta \neq 0 \iff \forall k \in \mathbb{Z},\ \theta \neq k \frac{\pi}{2}. $$$$

Lean4

theorem tan_ne_zero_iff {θ : ℝ} : tan θ ≠ 0 ↔ ∀ k : ℤ, k * π / 2 ≠ θ :=
  mod_cast @Complex.tan_ne_zero_iff θ

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru