two_nsmul_ne_zero_iff

Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

URI: https://scilib.ai/kg/mathlib#Real.Angle.two_nsmul_ne_zero_iff

English

For θ ∈ Angle, (2)•θ = 0 iff θ = 0 or θ = π.

Русский

Для θ ∈ угол, (2)•θ = 0 тогда, когда θ = 0 или θ = π.

LaTeX

$$$ (2 : \mathbb{Z}) \cdot \theta = 0 \\iff \theta = 0 \\lor \theta = \pi. $$$

Lean4

theorem two_nsmul_ne_zero_iff {θ : Angle} : (2 : ℕ) • θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ π := by rw [← not_or, ← two_nsmul_eq_zero_iff]

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

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

Разделы

Аффилиация

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