English
For each m ∈ M, the map r ↦ single(m,r) is an additive monoid hom from R to MonoidAlgebra R M.
Русский
Для каждого m ∈ M отображение r ↦ single(m,r) является аддитивным моноид-гомом из R в MonoidAlgebra R M.
LaTeX
$$$\\mathrm{singleAddHom}(m) : R \\rightarrow+ MonoidAlgebra(R,M)$ with \\toFun = \\mathrm{single}(m,\\cdot) and (map\\_zero' = single\\_zero m) and (map\\_add' = single\\_add m)$$$
Lean4
/-- `MonoidAlgebra.single` as an `AddMonoidHom`.
TODO: Rename to `singleAddMonoidHom`. -/
@[to_additive (attr := simps) /-- `AddMonoidAlgebra.single` as an `AddMonoidHom`.
TODO: Rename to `singleAddMonoidHom`. -/
]
def singleAddHom (m : M) : R →+ MonoidAlgebra R M
where
toFun := single m
map_zero' := single_zero _
map_add' := single_add _
