mFourier_add — Mathlib

English

For any m,n: d → Z and x ∈ UnitAddTorus, mFourier (m + n) x = mFourier m x · mFourier n x.

Русский

Для любых m,n: d → ℤ и x ∈ UnitAddTorus, mFourier (m+n) x = mFourier m x · mFourier n x.

LaTeX

$$$ mFourier (m + n) x = mFourier m x \cdot mFourier n x $$$

Lean4

theorem mFourier_add {m : d → ℤ} : mFourier (m + n) x = mFourier m x * mFourier n x := by
  simp only [mFourier, Pi.add_apply, fourier_add, ContinuousMap.coe_mk, ← Finset.prod_mul_distrib]

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