mathlib3

13d86df6 - chore(algebra/monoid_algebra): provide finer-grained levels of structure for less-structured `G`. (#6572)

chore(algebra/monoid_algebra): provide finer-grained levels of structure for less-structured `G`. (#6572) This provides `distrib` and `mul_zero_class` for when `G` is just `has_mul`, and `semigroup` for when `G` is just `semigroup`. It also weakens the typeclass assumptions on some correspondings lemmas.