fourier_add — Mathlib

English

For integers m, n and x ∈ AddCircle(T), the Fourier monomial is multiplicative: f_{m+n}(x) = f_m(x) f_n(x).

Русский

Для целых m, n и точки x ∈ AddCircle(T) мономиала Фурье удовлетворяет: f_{m+n}(x) = f_m(x) f_n(x).

LaTeX

$$$f_{m+n}(x) = f_m(x) \\cdot f_n(x) \\quad (m,n \\in \\mathbb{Z}, \\ x \\in AddCircle(T)).$$$

Lean4

theorem fourier_add {m n : ℤ} {x : AddCircle T} : fourier (m + n) x = fourier m x * fourier n x := by
  simp_rw [fourier_apply, add_zsmul, toCircle_add, Circle.coe_mul]

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