inl — Mathlib

English

There is a canonical left embedding inl: M →* M ∗ N given by m ↦ inl m, which preserves the monoid structure.

Русский

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

LaTeX

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

Lean4

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

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