exp_mul_I_antiperiodic — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem exp_mul_I_antiperiodic : Function.Antiperiodic (fun x => exp (x * I)) π := by
  simpa only [mul_inv_cancel_right₀ I_ne_zero] using exp_antiperiodic.mul_const I_ne_zero

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