natCoe — Mathlib

English

There is an instance making a natural-valued arithmetic function coerce into any monoid with one.

Русский

Существуют инстансы для переноса Nat-значений в ArithmeticFunction R в произвольный монойд с единицей.

LaTeX

$$$[\\text{AddMonoidWithOne } R] : Coe (ArithmeticFunction ℕ) (ArithmeticFunction R)$$$

Lean4

instance natCoe [AddMonoidWithOne R] : Coe (ArithmeticFunction ℕ) (ArithmeticFunction R) :=
  ⟨natToArithmeticFunction⟩

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