toZSMul

Mathlib.Algebra.Group.Defs

URI: https://scilib.ai/kg/mathlib#SubNegMonoid.toZSMul

English

A SubNegMonoid M carries a Z-action: there is an SMul ℤ M structure defined by zsmul.

Русский

У SubNegMonoid M имеется действие Z на M, задаваемое zsmul.

LaTeX

$$$\\forall n \\in \\mathbb{Z},\\ \\forall m \\in M,\\ n \\cdot m = zsmul(n,m)$$$

Lean4

instance toZSMul {M} [SubNegMonoid M] : SMul ℤ M :=
  ⟨SubNegMonoid.zsmul⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru