ofMagma — Mathlib

English

Embedding of a magma with zero into its magma algebra: each element m in M maps to the basis element single m 1 in R[M], and this map is compatible with magma multiplication.

Русский

Вставка магмы с нулём в её алгебру образуется отображением m ↦ single m 1, сохраняющим умножение.

LaTeX

$$$\\mathrm{OfMagma}_{R,M} : M \\to \\mathrm{MonoidHom}(M,R[M]),\\ a \\mapsto \\mathrm{single}(a,1).$$$

Lean4

/-- The embedding of an additive magma into its additive magma algebra. -/
@[simps]
def ofMagma [Add M] : Multiplicative M →ₙ* R[M]
    where
  toFun a := single a 1
  map_mul' a b := by simp only [mul_def, mul_one, sum_single_index, single_eq_zero, mul_zero]; rfl

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