scaled_exp_map_periodic — Mathlib

English

Exp r = Exp s if and only if r and s are congruent modulo 2π.

Русский

Exp r = Exp s эквивалентно тому, что r и s конгруентны по модулю 2π.

LaTeX

$$$$ \exp r = \exp s \iff r \equiv s \pmod{2\pi}. $$$$

Lean4

theorem scaled_exp_map_periodic : Function.Periodic (fun x => Circle.exp (2 * π / T * x)) T := by
  -- The case T = 0 is not interesting, but it is true, so we prove it to save hypotheses

  rcases eq_or_ne T 0 with (rfl | hT)
  · simp
  · intro x; simp_rw [mul_add]; rw [div_mul_cancel₀ _ hT, Circle.periodic_exp]

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