nSMul — Mathlib

English

An AddSubmonoid of an AddMonoid inherits a natural ℕ-scalar action: for any S, there is SMul ℕ S given by n • a = ⟨n • a.1, nsmul_mem a.2 n⟩.

Русский

Подмножество AddSubmonoid подAddMonoid наследует естественное действие скаляров ℕ: для любого S существует действие SMul ℕ на S, заданное n • a = ⟨n • a.1, nsmul_mem a.2 n⟩.

LaTeX

$${M} [AddMonoid M] {A : Type} [SetLike A M] [AddSubmonoidClass A M] (S : A) : SMul ℕ S$$

Lean4

/-- An `AddSubmonoid` of an `AddMonoid` inherits a scalar multiplication. -/
instance nSMul {M} [AddMonoid M] {A : Type*} [SetLike A M] [AddSubmonoidClass A M] (S : A) : SMul ℕ S :=
  ⟨fun n a => ⟨n • a.1, nsmul_mem a.2 n⟩⟩

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