hasNatPow — Mathlib

English

There is a natural-number scalar action on SimpleFunc α β when β is an additive monoid; n • f is defined pointwise.

Русский

Для любого α, β со скобками, существует действие натурального умножения на SimpleFunc α β, задаваемое по точкам.

LaTeX

$$$\\text{instance }\\text{hasNatSMul }[AddMonoid\\ β]: SMul\\ \\mathbb{N}\\ (\\alpha \\to_{S}\\ \\beta).$$$

Lean4

@[to_additive existing hasNatSMul]
instance hasNatPow [Monoid β] : Pow (α →ₛ β) ℕ :=
  ⟨fun f n => f.map (· ^ n)⟩

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