instMonoid

Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise

URI: https://scilib.ai/kg/mathlib#SubMulAction.instMonoid

English

If M is a Monoid, then SubMulAction R M is a Monoid with the natural product and unit.

Русский

Если M является моноидом, то SubMulAction R M образует моноид с естественным умножением и единицей.

LaTeX

$$$\\text{If } M\\text{ is a Monoid, then SubMulAction } R M\\text{ is a Monoid}.$$$

Lean4

instance : Monoid (SubMulAction R M) :=
  { }

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

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

Разделы

Аффилиация

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