mul_apply_one

Mathlib.NumberTheory.ArithmeticFunction

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

English

Special value of Dirichlet convolution at n = 1: (f * g)(1) = f(1) g(1).

Русский

Особое значение свёртки Дирихле в точке 1: (f * g)(1) = f(1) g(1).

LaTeX

$$$(f * g)(1) = f(1) \\cdot g(1)$$$

Lean4

theorem mul_apply_one [Semiring R] {f g : ArithmeticFunction R} : (f * g) 1 = f 1 * g 1 := by simp

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

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

Разделы

Аффилиация

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