natCoe_apply — Mathlib

English

Let f be an arithmetic function with natural values and x a natural number. Then the value of the coerced function at x equals the original value: (f : ArithmeticFunction R) x = f x.

Русский

Пусть f — арифметическая функция с значениями в ℕ, и x — натуральное число. Тогда значение приводной функции в точке x равно исходному: (f : ArithmeticFunction R) x = f x.

LaTeX

$$$(f : \\mathrm{ArithmeticFunction}\\, R)(x) = f(x)$$$

Lean4

@[simp]
theorem natCoe_apply [AddMonoidWithOne R] {f : ArithmeticFunction ℕ} {x : ℕ} : (f : ArithmeticFunction R) x = f x :=
  rfl

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