ofMagma — Mathlib

English

The embedding sends each element a ∈ M to the basis element single a 1 in MonoidAlgebra R M.

Русский

Встраивание отображает элемент a ∈ M в базисный элемент single a 1 в MonoidAlgebra R M.

LaTeX

$$$\operatorname{ofMagma}(a) = \operatorname{single}(a,1)$$$

Lean4

/-- The embedding of a magma into its magma algebra. -/
@[simps]
def ofMagma : M →ₙ* MonoidAlgebra 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]

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