English
There is an algebra equivalence between AddMonoidAlgebra k G and MonoidAlgebra k (Multiplicative G) that expresses AddMonoidAlgebra in multiplicative form.
Русский
Существует алгебраическое эквивалентное соответствие между AddMonoidAlgebra k G и MonoidAlgebra k (Multiplicative G) по смыслу в форме множителей.
LaTeX
$$$\\text{toMultiplicativeAlgEquiv} : AddMonoidAlgebra\\, k\\, G \\simeq_A\\, MonoidAlgebra\\, k\\, (Multiplicative\\, G).$$$
Lean4
/-- The algebra equivalence between `AddMonoidAlgebra` and `MonoidAlgebra` in terms of
`Multiplicative`. -/
def toMultiplicativeAlgEquiv [Semiring k] [Algebra R k] [AddMonoid G] :
AddMonoidAlgebra k G ≃ₐ[R] MonoidAlgebra k (Multiplicative G) :=
{ AddMonoidAlgebra.toMultiplicative k G with commutes' := fun r => by simp [AddMonoidAlgebra.toMultiplicative] }
