exp_antiperiodic — Mathlib

English

Let z be a complex number. Then the complex exponential satisfies an antiperiodicity with period πi: exp(z + πi) = −exp(z) for all z ∈ ℂ.

Русский

Пусть z — комплексное число. Тогда экспонента по комплексным числам обладает антиперiodичностью с периодом πi: exp(z + πi) = −exp(z) для всех z ∈ ℂ.

LaTeX

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

Lean4

theorem exp_antiperiodic : Function.Antiperiodic exp (π * I) := by simp [exp_add, exp_mul_I]

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