mul_convolution_distrib — Mathlib

English

Twisting by a Dirichlet character χ distributes over Dirichlet convolution: (χ·f) * (χ·g) = χ·(f * g).

Русский

Утверждение о распределении поворота χ над сверткой по Дирихле: (χ·f) * (χ·g) = χ·(f * g).

LaTeX

$$$((\chi \cdot) * f) * ((\chi \cdot) * g) = (\chi \cdot) * (f * g).$$$

Lean4

/-- Twisting by a Dirichlet character `χ` distributes over convolution. -/
theorem mul_convolution_distrib {R : Type*} [CommSemiring R] {n : ℕ} (χ : DirichletCharacter R n) (f g : ℕ → R) :
    (((χ ·) : ℕ → R) * f) ⍟ (((χ ·) : ℕ → R) * g) = ((χ ·) : ℕ → R) * (f ⍟ g) :=
  by
  ext n
  simp only [Pi.mul_apply, LSeries.convolution_def, Finset.mul_sum]
  refine Finset.sum_congr rfl fun p hp ↦ ?_
  rw [(mem_divisorsAntidiagonal.mp hp).1.symm, cast_mul, map_mul]
  exact mul_mul_mul_comm ..

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