instIsCancelMulMonoidHom

Mathlib.Algebra.Group.Hom.Instances

URI: https://scilib.ai/kg/mathlib#instIsCancelMulMonoidHom

English

If M is a MulOneClass and N a Monoid with IsCancelMul, then MonoidHom M N is IsCancelMul.

Русский

Если M — MulOneClass, N — моноид с IsCancelMul, то MonoidHom M N имеет IsCancelMul.

LaTeX

$$$\mathrm{IsCancelMul}(\mathrm{MonoidHom}\,M\,N).$$$

Lean4

@[to_additive]
instance [MulOneClass M] [CommMonoid N] [IsCancelMul N] : IsCancelMul (M →* N) where

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

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

Разделы

Аффилиация

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