coe_mul — Mathlib

English

The product of two arithmetic functions defines the same function as the Dirichlet convolution.

Русский

Произведение двух арифметических функций задаёт ту же самую функцию, что и дирихлетова свёртка.

LaTeX

$$$f \\star g = \\text{the function underlying } f * g$.$$

Lean4

/-- The product of two arithmetic functions defines the same function as the Dirichlet convolution
of the functions defined by them. -/
theorem coe_mul {R : Type*} [Semiring R] (f g : ArithmeticFunction R) : f ⍟ g = ⇑(f * g) := by simp [convolution]

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