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