English
There is a coercion from ArithmeticFunction ℤ to ArithmeticFunction R, defined by ofInt, sending f to the function n ↦ ↑(f n).
Русский
Существует переходное отображение из ArithmeticFunction ℤ в ArithmeticFunction R, заданное через ofInt: f ↦ (n ↦ ↑(f(n))).
LaTeX
$$$\\mathrm{intCoe}: \\mathrm{ArithmeticFunction}(\\mathbb{Z}) \\to \\mathrm{ArithmeticFunction}(R)$ with $(\\mathrm{intCoe}\, f)(n) = \\uparrow (f(n))$$$
Lean4
instance intCoe [AddGroupWithOne R] : Coe (ArithmeticFunction ℤ) (ArithmeticFunction R) :=
⟨ofInt⟩