delta_mul

Mathlib.NumberTheory.LSeries.Dirichlet

URI: https://scilib.ai/kg/mathlib#DirichletCharacter.delta_mul

English

The Dirichlet convolution of a Dirichlet character χ with its twist by μ yields the delta function: (χ·) * (χ·μ) = δ.

Русский

Свёртка Дирихле χ с поворотом χ·μ дает δ: (χ·) * (χ·μ) = δ.

LaTeX

$$$(\chi \cdot) * (\chi \cdot \mu) = \delta.$$$

Lean4

theorem delta_mul {n : ℕ} (χ : DirichletCharacter ℂ n) : δ * ↗χ = δ :=
  mul_comm δ _ ▸ mul_delta ..

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru