natCoe_nat — Mathlib

English

Let f be an arithmetic function valued in the natural numbers. Then applying the natural-to-arithmetic-function embedding yields the same function; i.e., natToArithmeticFunction f = f.

Русский

Пусть f — арифметическая функция со значениями в натуральных числах. Тогда вложение natToArithmeticFunction f = f.

LaTeX

$$$\\forall f:\\mathrm{ArithmeticFunction}(\\mathbb{N}), \\ operatorname{natToArithmeticFunction}(f) = f$$$

Lean4

@[simp]
theorem natCoe_nat (f : ArithmeticFunction ℕ) : natToArithmeticFunction f = f :=
  ext fun _ => cast_id _

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