intCoe — Mathlib

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⟩

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