English
Let M and N be monoids. The natural projection fst: M × N → M is a monoid homomorphism, sending (m,n) to m; it preserves identity and multiplication.
Русский
Пусть M и N — моноиды. Натуральная проекция fst: M × N → M является гомоморфизмом моноидов, отправляющим (m,n) в m; сохраняет единицу и умножение.
LaTeX
$$$ \\operatorname{fst}: M \\times N \\to M \\text{ is a monoid homomorphism, i.e. } \\operatorname{fst}((m_1,n_1)\\cdot(m_2,n_2)) = \\operatorname{fst}(m_1,n_1)\\operatorname{fst}(m_2,n_2) \\text{ and } \\operatorname{fst}(1,1) = 1. $$$
Lean4
/-- Given monoids `M`, `N`, the natural projection homomorphism from `M × N` to `M`. -/
@[to_additive /-- Given additive monoids `A`, `B`, the natural projection homomorphism
from `A × B` to `A` -/
]
def fst : M × N →* M :=
{ toFun := Prod.fst, map_one' := rfl, map_mul' := fun _ _ => rfl }
