coe_eq_zero_iff — Mathlib

English

For any real x, x as an angle equals 0 if and only if x is an integer multiple of 2π.

Русский

Для любого действительного x равенство x как угол нулю эквивалентно тому, что x является целым кратным 2π.

LaTeX

$$$$ (x:\mathbb{R}) \;\text{in Angle} = 0 \ \iff \ \exists n \in \mathbb{Z},\; n\cdot(2\pi) = x. $$$$

Lean4

theorem coe_eq_zero_iff {x : ℝ} : (x : Angle) = 0 ↔ ∃ n : ℤ, n • (2 * π) = x :=
  AddCircle.coe_eq_zero_iff (2 * π)

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