exp_mul_I_periodic — Mathlib

English

The function x ↦ exp(i x) is periodic with period 2π: exp(i(x + 2π)) = exp(i x) for all real x.

Русский

Функция x ↦ exp(i x) периодична по периоду 2π: exp(i(x + 2π)) = exp(i x) для всех действительных x.

LaTeX

$$$$ \\forall x \\in \\mathbb{R}, \\; \\exp(i x + 2\\pi i) = \\exp(i x). $$$$

Lean4

theorem exp_mul_I_periodic : Function.Periodic (fun x => exp (x * I)) (2 * π) :=
  exp_mul_I_antiperiodic.periodic_two_mul

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