English
There is a canonical way to view an integer-valued arithmetic function as a function with values in any target ring R: (ArithmeticFunction ℤ) → (ArithmeticFunction R) given by f ↦ (n ↦ ↑(f n)).
Русский
Существует каноническое отображение ℤ-значных арифметических функций в арифметические функции с значениями в R: f ↦ (n ↦ ↑(f n)).
LaTeX
$$$\\mathrm{ofInt}: \\mathrm{ArithmeticFunction}(\\mathbb{Z}) \\to \\mathrm{ArithmeticFunction}(R), \\quad (\\mathrm{ofInt} \\, f)(n) = \\uparrow (f(n))$$$
Lean4
/-- Coerce an arithmetic function with values in `ℤ` to one with values in `R`. We cannot inline
this in `intCoe` because it gets unfolded too much. -/
@[coe]
def ofInt [AddGroupWithOne R] : (ArithmeticFunction ℤ) → (ArithmeticFunction R) := fun f => ⟨fun n => ↑(f n), by simp⟩
