exp_periodic — Mathlib

English

Let z be a complex number. The complex exponential has period 2πi: exp(z + 2πi) = exp(z) for all z ∈ ℂ.

Русский

Пусть z — комплексное число. Экспонента по комплексному числу имеет период 2πi: exp(z + 2πi) = exp(z) для всех z ∈ ℂ.

LaTeX

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

Lean4

theorem exp_periodic : Function.Periodic exp (2 * π * I) :=
  (mul_assoc (2 : ℂ) π I).symm ▸ exp_antiperiodic.periodic_two_mul

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