English
Let N > 0. If Φ: ZMod N → E and r is a scalar from a ring R that acts distributively on E and commutes with complex scalars, then the discrete Fourier transform is linear in Φ: 𝓕(r · Φ) = r · 𝓕Φ.
Русский
Пусть N>0. Для любой функции Φ: ZMod N → E и скаляра r из кольца R, действующего на E линейно и коммутирующего с комплексными скалярами, дискретное преобразование Фурье линейно по Φ: 𝓕(r · Φ) = r · 𝓕Φ.
LaTeX
$$$\\\\mathcal{F}(r \\\\cdot \\\\Phi) = r \\\\cdot \\\\mathcal{F}(\\\\Phi)$$$
Lean4
theorem dft_const_smul {R : Type*} [DistribSMul R E] [SMulCommClass R ℂ E] (r : R) (Φ : ZMod N → E) :
𝓕 (r • Φ) = r • 𝓕 Φ := by simp only [Pi.smul_def, dft_def, smul_sum, smul_comm]
