English
Let Φ: ZMod N → R and e ∈ E, where R acts on itself and on E compatibly with the complex scalar structure. Then 𝓕(j ↦ Φ(j) • e) = k ↦ 𝓕Φ(k) • e; i.e., the Fourier transform commutes with scalar action pointwise.
Русский
Пусть Φ: ZMod N → R и есть постоянный элемент e ∈ E; тогда 𝓕(Φ(j) • e) = 𝓕(Φ)(k) • e для всех k, то есть преобразование Фурье сохраняет скалярное действие по пунктам.
LaTeX
$$$\\mathcal{F}(j \\mapsto \\Phi(j) \\cdot e) = (\\mathcal{F}\\Phi) \\cdot e$$$
Lean4
theorem dft_smul_const {R : Type*} [Ring R] [Module ℂ R] [Module R E] [IsScalarTower ℂ R E] (Φ : ZMod N → R) (e : E) :
𝓕 (fun j ↦ Φ j • e) = fun k ↦ 𝓕 Φ k • e := by simp only [dft_def, sum_smul, smul_assoc]
