two_zsmul_ne_zero_iff

Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

English

For θ ∈ Angle, (2)•θ ≠ 0 iff θ ≠ 0 and θ ≠ π.

Русский

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

LaTeX

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

Lean4

theorem two_zsmul_ne_zero_iff {θ : Angle} : (2 : ℤ) • θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ π := by rw [← not_or, ← two_zsmul_eq_zero_iff]

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

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

Разделы

Аффилиация

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