zeta_mul_comm

Mathlib.NumberTheory.ArithmeticFunction

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

English

For any arithmetic function f with Nat-values, the Dirichlet convolution with ζ is commutative: ζ * f = f * ζ.

Русский

Для любой арифметической функции f со значениями в ℕ, Дирихлетова свёртка ζ коммутирует: ζ * f = f * ζ.

LaTeX

$$$$ \zeta * f = f * \zeta $$$$

Lean4

theorem zeta_mul_comm {f : ArithmeticFunction ℕ} : ζ * f = f * ζ := by rw [← natCoe_nat ζ, coe_zeta_mul_comm]

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

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

Разделы

Аффилиация

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