periodic_exp — Mathlib

English

The exponential map to the unit circle is periodic with period 2π: exp(t + 2π) = exp(t) for all t.

Русский

Экспоненциальное отображение на единичной окружности периодично с периодом 2π: для любого t выполняется exp(t + 2π) = exp(t).

LaTeX

$$$$ \exp(x + 2\pi) = \exp x \quad \text{for all } x \in \mathbb{R}. $$$$

Lean4

theorem periodic_exp : Periodic exp (2 * π) := fun z ↦ exp_eq_exp.2 ⟨1, by rw [Int.cast_one, one_mul]⟩

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