fourier_eval_zero — Mathlib

English

For any integer n, the value of f_n at the origin of AddCircle(T) is 1: f_n(0) = 1.

Русский

Для любого целочисленного n значения мономиалы Фурье в начале AddCircle(T) равны 1: f_n(0) = 1.

LaTeX

$$$f_n(0) = 1 \\quad (n \\in \\mathbb{Z}).$$$

Lean4

theorem fourier_eval_zero (n : ℤ) : fourier n (0 : AddCircle T) = 1 := by
  rw [← QuotientAddGroup.mk_zero, fourier_coe_apply, Complex.ofReal_zero, mul_zero, zero_div, Complex.exp_zero]

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