dft_const_mul — Mathlib

English

If Φ: ZMod N → R and r ∈ R, then multiplying Φ by a scalar on the left commutes with the DFT: 𝓕(j ↦ r · Φ(j)) = (k ↦ 𝓕Φ(k)) · r.

Русский

Пусть Φ: ZMod N → R и скаляр r слева. Тогда 𝓕(Φ(j) · r) = 𝓕Φ(k) · r.

LaTeX

$$$\\\\mathcal{F}(j \\mapsto r \\\\cdot \\\\Phi(j)) = (k \\mapsto \\\\mathcal{F}\\\\Phi(k)) \\\\cdot r$$$

Lean4

theorem dft_const_mul {R : Type*} [Ring R] [Algebra ℂ R] (r : R) (Φ : ZMod N → R) :
    𝓕 (fun j ↦ r * Φ j) = fun k ↦ r * 𝓕 Φ k :=
  dft_const_smul r Φ

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