circleMap_eq_circleMap_iff — Mathlib

English

circleMap c R a = circleMap c R b holds exactly when there exists n ∈ ℤ with a I = b I + n (2π I).

Русский

circleMap c R a = circleMap c R b тогда и только тогда, когда существует n ∈ ℤ such that a I = b I + n (2π I).

LaTeX

$$$ circleMap c R a = circleMap c R b \iff \exists n \in \mathbb{Z},\ a I = b I + n (2 \pi I) $$$

Lean4

theorem circleMap_eq_circleMap_iff {a b R : ℝ} (c : ℂ) (h_R : R ≠ 0) :
    circleMap c R a = circleMap c R b ↔ ∃ (n : ℤ), a * I = b * I + n * (2 * π * I) :=
  by
  have : circleMap c R a = circleMap c R b ↔ (exp (a * I)).arg = (exp (b * I)).arg := by
    simp [circleMap, ext_norm_arg_iff, h_R]
  simp [this, arg_eq_arg_iff, exp_eq_exp_iff_exists_int]

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