inr — Mathlib

English

There is a canonical right embedding inr: N →* M ∗ N given by n ↦ inr n, which preserves the monoid structure.

Русский

Существует каноническое правое вложение inr: N →* M ∗ N, заданное n ↦ inr n, сохраняющее структуру моноида.

LaTeX

$$$ inr: N \to M \ast N \quad\text{is a monoid hom with } inr(nm) = inr(n) \cdot inr(m),\; inr(1)=1.$$$

Lean4

/-- The natural embedding `N →* M ∗ N`. -/
@[to_additive /-- The natural embedding `N →+ AddMonoid.Coprod M N`. -/
    ]
def inr : N →* M ∗ N where
  toFun := fun x => mk (of (.inr x))
  map_one' := mk_eq_mk.2 fun _c hc => hc.2.2.2
  map_mul' := fun x y => mk_eq_mk.2 fun _c hc => hc.2.1 x y

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