Zulip Chat Archive

Stream: new members

Topic: Group ring?

Sophia Rodriguez (Mar 13 2025 at 05:57):

Do we have group ring in mathlib? I want to prove that for any commutative ring $R$ and any abelian group $G$ , the group ring $RG$ is a commutative ring. But got stuck at the very beginning.

Johan Commelin (Mar 13 2025 at 06:00):

See docs#MonoidAlgebra

Sophia Rodriguez (Mar 13 2025 at 06:03):

Great! exactly what I want

Last updated: May 02 2025 at 03:31 UTC