of — Mathlib · SciLib

English

The embedding of a monoid G into SkewMonoidAlgebra k G is given by a ↦ single a 1 and is a monoid homomorphism mapping product to skew multiplication.

Русский

Встраивание моноида G в SkewMonoidAlgebra k G задаётся как a ↦ single a 1 и является гомоморфизмом моноидов, отображающим произведение в skew-произведение.

LaTeX

$$$\mathrm{of} : G \to \mathrm{SkewMonoidAlgebra}(k,G),\quad \mathrm{of}(a) = \mathrm{single}(a,1)$$$

Lean4

/-- The embedding of a monoid into its skew monoid algebra. -/
def of : G →* SkewMonoidAlgebra k G where
  toFun a := single a 1
  map_one' := rfl
  map_mul' a b := by simp

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