mathlib3

feat(data/monoid_algebra): some lemmas about group rings

#2239

Merged