instIsMonHomFst

Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_

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

English

The projection fst: M ⊗ N → M is a monoid hom, i.e., preserves the monoid structure in the first factor.

Русский

Проекция fst: M ⊗ N → M является мономорфизмом, то есть сохраняет моноидную структуру в первой компоненте.

LaTeX

$$$\\text{fst}(M,N): M \\otimes N \\to M$ is a monoid hom$$

Lean4

instance : IsMonHom (fst M N) where

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

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

Разделы

Аффилиация

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