English
Let M,N be monoids. The natural inclusion inr: N →* M × N maps n to (1,n), providing the right embedding of N into the product.
Русский
Пусть M,N — моноиды. Натуральное включение inr: N →* M × N отправляет n в (1,n), образуя правую вложенность N в произведение.
LaTeX
$$$ \\operatorname{inr}: N \\to M \\times N ,\\quad \\operatorname{inr}(n) = (1,n). $$$
Lean4
/-- Given monoids `M`, `N`, the natural inclusion homomorphism from `N` to `M × N`. -/
@[to_additive /-- Given additive monoids `A`, `B`, the natural inclusion homomorphism
from `B` to `A × B`. -/
]
def inr : N →* M × N :=
{ toFun := fun y => (1, y), map_one' := rfl, map_mul' := fun _ _ => Prod.ext (one_mul 1).symm rfl }
