how to define a group ring

Stream: new members

[Chengyan Hu]

Hi! I want to claim an isomorphism of modules over a group ring, but I'm confused in how group rings work in lean. Can anyone give me some help in how to define a group ring?

[Junyan Xu]

Short answer: k[G] is MonoidAlgebra k G.
It might be instructive to check how the Maschke theorem file works.

[Aaron Liu]

docs#MonoidAlgebra