instIsMonHomLift

Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_

URI: https://scilib.ai/kg/mathlib#MonObj.instIsMonHomLift

English

If f: M → N and g: M → O are monoid homomorphisms, then lift f g is a monoid homomorphism.

Русский

Если f: M → N и g: M → O — мономорфизмы, то lift f g — мономорфизм.

LaTeX

$$$\\text{lift} f g : M \\to N \\otimes O$ is a monoid hom$$

Lean4

instance {f : M ⟶ N} {g : M ⟶ O} [IsMonHom f] [IsMonHom g] : IsMonHom (lift f g) where

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

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

Разделы

Аффилиация

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