bernoulli_zero_fourier_coeff — Mathlib

English

For any nonzero integer n, bernoulliFourierCoeff 0 n = 0; i.e., the k = 0 case has zero Fourier coefficients for n ≠ 0.

Русский

Для любого ненулевого целого n, bernoulliFourierCoeff 0 n = 0; коэффициенты при k = 0 равны нулю для n ≠ 0.

LaTeX

$$$$ bernoulliFourierCoeff(0,n) = 0 \\quad( n \\neq 0 ). $$$$

Lean4

/-- The Fourier coefficients of `B₀(x) = 1`. -/
theorem bernoulli_zero_fourier_coeff {n : ℤ} (hn : n ≠ 0) : bernoulliFourierCoeff 0 n = 0 := by
  simpa using bernoulliFourierCoeff_recurrence 0 hn

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