English
There is a MonoidHom from the product R × M into MonoidAlgebra R M given by (r,m) ↦ single m r, i.e., mapping the pair to a single basis element with coefficient r.
Русский
Существует моноидоморфизм из произведения R × M в MonoidAlgebra R M, задаваемый (r,m) ↦ single m r.
LaTeX
$$$\operatorname{singleHom} : (R \times M) \to* MonoidAlgebra\; R\; M$ with $\operatorname{toFun}(a,b) = \operatorname{single}(b,a)$$$
Lean4
/-- `MonoidAlgebra.single` as a `MonoidHom` from the product type into the monoid algebra.
Note the order of the elements of the product are reversed compared to the arguments of
`MonoidAlgebra.single`. -/
@[simps]
def singleHom : R × M →* MonoidAlgebra R M where
toFun a := single a.2 a.1
map_one' := rfl
map_mul' _a _b := by simp
