natToArithmeticFunction — Mathlib

English

Coerce an arithmetic function with values in ℕ to one with values in R by applying the natural embedding to each value.

Русский

Приведение арифметической функции с значениями в ℕ к значениям в R через естественную вложенность.

LaTeX

$$$\\text{natToArithmeticFunction}([A]) : ArithmeticFunction ℕ \\to ArithmeticFunction R,\\quad (\\text{natToArithmeticFunction}(f))(n) = \\uparrow(f(n))$$$

Lean4

/-- Coerce an arithmetic function with values in `ℕ` to one with values in `R`. We cannot inline
this in `natCoe` because it gets unfolded too much. -/
@[coe]
def natToArithmeticFunction [AddMonoidWithOne R] : (ArithmeticFunction ℕ) → (ArithmeticFunction R) := fun f =>
  ⟨fun n => ↑(f n), by simp⟩

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