instNSmul — Mathlib

English

If M is an additive monoid with a continuous addition, then SeparationQuotient M carries a natural-number scalar action.

Русский

Если M — аддитивный мономод с непрерывным сложением, то SeparationQuotient(M) имеет естественное действие натуральных чисел.

LaTeX

$$$\operatorname{SMul}\mathbb{N}(\mathrm{SeparationQuotient}(M))$$$

Lean4

instance (priority := 900) instNSmul [AddMonoid M] [ContinuousAdd M] : SMul ℕ (SeparationQuotient M) :=
  inferInstance

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