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 ..