mul_delta_eq_smul_delta

Mathlib.NumberTheory.LSeries.Basic

URI: https://scilib.ai/kg/mathlib#LSeries.mul_delta_eq_smul_delta

English

For any f, f * δ = f(1) • δ.

Русский

Для любой f: f * δ = f(1) · δ.

LaTeX

$$∀ {f}, f * δ = f(1) • δ$$

Lean4

theorem mul_delta_eq_smul_delta {f : ℕ → ℂ} : f * δ = f 1 • δ :=
  by
  ext n
  by_cases hn : n = 1 <;> simp [hn, delta]

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

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

Разделы

Аффилиация

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