sign_two_zsmul_eq_sign_iff — Mathlib

English

The equality ((2)•θ).sign = θ.sign holds iff θ = π or |θ.toReal| < π/2.

Русский

Равенство ((2)•θ).sign = θ.sign верно тогда и только тогда, когда θ = π или |θ.toReal| < π/2.

LaTeX

$$((2:\,\mathbb{Z})\cdot θ).\text{sign} = θ.\text{sign} \iff θ = π \lor |θ.toReal| < π/2$$

Lean4

theorem sign_two_zsmul_eq_sign_iff {θ : Angle} : ((2 : ℤ) • θ).sign = θ.sign ↔ θ = π ∨ |θ.toReal| < π / 2 := by
  rw [two_zsmul, ← two_nsmul, sign_two_nsmul_eq_sign_iff]

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