dft_mul_const — Mathlib

English

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

Русский

Если Φ: ZMod N → R и скаляр r, то 𝓕(j ↦ Φ(j) · r) = k ↦ 𝓕Φ(k) · r.

LaTeX

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

Lean4

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

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