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