toArithmeticFunction — Mathlib

English

Applying toArithmeticFunction to an ArithmeticFunction yields the same arithmetic function.

Русский

Применение toArithmeticFunction к арифметической функции возвращает ту же арифметическую функцию.

LaTeX

$$$\\operatorname{toArithmeticFunction}(f)=f\\quad\\text{for all } f\\in\\text{ArithmeticFunction R}. $$$

Lean4

/-- We turn any function `ℕ → R` into an `ArithmeticFunction R` by setting its value at `0`
to be zero. -/
def toArithmeticFunction {R : Type*} [Zero R] (f : ℕ → R) : ArithmeticFunction R
    where
  toFun n := if n = 0 then 0 else f n
  map_zero' := rfl

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