toNatModule — Mathlib

English

Any AddCommMonoid M carries a natural-number module structure, i.e., a canonical action of ℕ on M making M a module over the natural numbers by repeated addition.

Русский

Для любой AddCommMonoid M существует каноническая структура модуля над натуральными числами: ℕ действует на M путём повторного сложения.

LaTeX

$$$\text{Module}_{\mathbb{N}} \;M$ with $n \cdot m = m + \cdots + m$ ($n$ times)$$

Lean4

instance toNatModule : Module ℕ M where
  one_smul := one_nsmul
  mul_smul m n a := mul_nsmul' a m n
  smul_add n a b := nsmul_add a b n
  smul_zero := nsmul_zero
  zero_smul := zero_nsmul
  add_smul r s x := add_nsmul x r s

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