instSMul

Mathlib.Algebra.Group.Action.Units

URI: https://scilib.ai/kg/mathlib#Units.instSMul

English

There is a natural SMul instance of Units M on α defined by m • a := (m : M) • a.

Русский

Существует естественное действие Units M на α: m • a := (m : M) • a.

LaTeX

$$$ SMul \\text{Units } M \\; \\alpha,\\; (m:\\mathrm{Units}M)\\; a := (m: M) • a$$$

Lean4

@[to_additive]
instance [Monoid M] [SMul M α] : SMul Mˣ α where smul m a := (m : M) • a

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

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

Разделы

Аффилиация

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