one_eq_delta

Mathlib.NumberTheory.LSeries.Dirichlet

URI: https://scilib.ai/kg/mathlib#ArithmeticFunction.one_eq_delta

← MathLib Explorer

English

The L-series of the constant function 1 corresponds to the delta function δ.

Русский

L‑серия константной функции 1 равна δ.

LaTeX

$$↗(1 : ArithmeticFunction ℂ) = δ$$

Lean4

/-- `δ` is the function underlying the arithmetic function `1`. -/
theorem one_eq_delta : ↗(1 : ArithmeticFunction ℂ) = δ := by
  ext
  simp [one_apply, LSeries.delta]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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