dft_comp_unitMul — Mathlib

English

Let Φ: ZMod N → E, u ∈ (ZMod N)ˣ be a unit, and k ∈ ZMod N. Then 𝓕(j ↦ Φ(u.val · j))(k) = 𝓕Φ(u⁻¹.val · k).

Русский

Пусть Φ: ZMod N → E и u — единичный элемент кольца ZMod N; тогда 𝓕(Φ(u·j))(k) = 𝓕Φ(u⁻¹·k).

LaTeX

$$$\\\\mathcal{F}(j \\mapsto \\Phi(u.\\\\val \\cdot j))(k) = \\\\mathcal{F}\\\\Phi( (u^{-1}).\\\\val \\cdot k)$$$

Lean4

theorem dft_comp_unitMul (Φ : ZMod N → E) (u : (ZMod N)ˣ) (k : ZMod N) :
    𝓕 (fun j ↦ Φ (u.val * j)) k = 𝓕 Φ (u⁻¹.val * k) :=
  by
  refine Fintype.sum_equiv u.mulLeft _ _ fun x ↦ ?_
  simp only [mul_comm u.val, u.mulLeft_apply, ← mul_assoc, u.mul_inv_cancel_right]

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