arg_toCircle — Mathlib

English

For a real number r, exp r = 1 if and only if r is an integer multiple of 2π.

Русский

Для вещественного числа r верно: exp r = 1 тогда и только тогда, когда r = n·2π, n ∈ ℤ.

LaTeX

$$$$ \exp r = 1 \iff \exists n \in \mathbb{Z},\ r = n\cdot(2\pi). $$$$

Lean4

@[simp]
theorem arg_toCircle (θ : Real.Angle) : (arg θ.toCircle : Angle) = θ :=
  by
  induction θ using Real.Angle.induction_on
  rw [toCircle_coe, Circle.coe_exp, exp_mul_I, ← ofReal_cos, ← ofReal_sin, ← Real.Angle.cos_coe, ← Real.Angle.sin_coe,
    arg_cos_add_sin_mul_I_coe_angle]

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