mul_delta

Mathlib.NumberTheory.LSeries.Dirichlet

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

English

The delta function is a left-identity for twisting: δ * (χ·) = δ.

Русский

Дельта-функция является левым единичным элементом для поворота: δ * (χ·) = δ.

LaTeX

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

Lean4

theorem mul_delta {n : ℕ} (χ : DirichletCharacter ℂ n) : ↗χ * δ = δ :=
  LSeries.mul_delta <| by rw [cast_one, map_one]

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

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

Разделы

Аффилиация

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