toNatSMul — Mathlib

English

On any AddMonoid M, there is a natural-scalar action of ℕ given by nsmul: n • x = x + x + ... + x (n times).

Русский

На любом AddMonoid M существует естественное действие множителя ℕ: n • x — сумма x, повторяющаяся n раз.

LaTeX

$$$\\forall M\\,[AddMonoid M],\\forall x\\in M,\\forall n\\in \\mathbb{N}: n \\cdot x = \\underbrace{x+\\cdots+x}_{n\\text{ times}}$$$

Lean4

instance toNatSMul {M : Type*} [AddMonoid M] : SMul ℕ M :=
  ⟨AddMonoid.nsmul⟩

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