Commit 2021-03-31 21:24 5f1b4500View on Github →
refactor(algebra/*): add new
add_zero_class for non-associative monoids (#6865)
This extracts a base class from
mul_one_class M, that drops the associativity assumption.
It goes on to weaken
submonoid to require
mul_one_class M instead of
monoid M, along with weakening the typeclass requirements for other primitive constructions like
Instances of the new classes are provided on
This is by no means an exhaustive relaxation across mathlib, but it aims to broadly cover the foundations.