English
There is a ring equivalence between AddMonoidAlgebra k G and MonoidAlgebra k (Multiplicative G) turning multiplication into the multiplicative structure.
Русский
Существует кольцевая эквивалентность между AddMonoidAlgebra k G и MonoidAlgebra k (Multiplicative G), переводящую умножение в мультипликативную структуру.
LaTeX
$$$ AddMonoidAlgebra.kG \simeq\! MonoidAlgebra k (Multiplicative G) $$$
Lean4
/-- The equivalence between `AddMonoidAlgebra` and `MonoidAlgebra` in terms of
`Multiplicative` -/
protected def toMultiplicative [Semiring k] [Add G] : AddMonoidAlgebra k G ≃+* MonoidAlgebra k (Multiplicative G)
where
__ := Finsupp.domCongr Multiplicative.ofAdd
toFun := equivMapDomain Multiplicative.ofAdd
map_mul' x
y := by
repeat' rw [equivMapDomain_eq_mapDomain (M := k)]
dsimp [Multiplicative.ofAdd]
exact MonoidAlgebra.mapDomain_mul (M := Multiplicative G) (MulHom.id (Multiplicative G)) x y
