mathlib

5f1b4500 - refactor(algebra/*): add new `mul_one_class` and `add_zero_class` for non-associative monoids (#6865)

refactor(algebra/*): add new `mul_one_class` and `add_zero_class` for non-associative monoids (#6865) This extracts a base class from `monoid M`, `mul_one_class M`, that drops the associativity assumption. It goes on to weaken `monoid_hom` and `submonoid` to require `mul_one_class M` instead of `monoid M`, along with weakening the typeclass requirements for other primitive constructions like `monoid_hom.fst`. Instances of the new classes are provided on `pi`, `prod`, `finsupp`, `(add_)submonoid`, and `(add_)monoid_algebra`. This is by no means an exhaustive relaxation across mathlib, but it aims to broadly cover the foundations.