mathlib

97118b45 - fix(algebra/group/commute): use the right typeclass (#7389)

fix(algebra/group/commute): use the right typeclass (#7389) This section is called `mul_one_class`, but I forgot to actually make it use `mul_one_class` instead of `monoid` in a previous PR...