coe_mk — Mathlib

English

There is a canonical way to regard an arithmetic function as a zero-homomorphism to R, giving a function-valued map.

Русский

Существует канонический способ рассмотреть арифметическую функцию как нулевой гомоморфизм в R.

LaTeX

$$$\\text{coe\_mk}$ is the defining equality between a ZeroHom and its underlying function.$$

Lean4

@[simp]
theorem coe_mk (f : ℕ → R) (hf) : @DFunLike.coe (ArithmeticFunction R) _ _ _ (ZeroHom.mk f hf) = f :=
  rfl

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