Commit 2021-03-31 21:24 5f1b4500

View on Github →

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.

Estimated changes

modified structure add_monoid_hom
modified theorem monoid_hom.cancel_left
modified theorem monoid_hom.cancel_right
modified theorem monoid_hom.coe_comp
modified theorem monoid_hom.coe_inj
modified theorem monoid_hom.coe_mk
modified def monoid_hom.comp
modified theorem monoid_hom.comp_apply
modified theorem monoid_hom.comp_assoc
modified def monoid_hom.comp_hom
modified theorem monoid_hom.comp_id
modified theorem monoid_hom.comp_inv
modified theorem monoid_hom.comp_mul
modified theorem monoid_hom.comp_one
modified theorem monoid_hom.congr_arg
modified theorem monoid_hom.congr_fun
modified theorem monoid_hom.div_apply
modified def monoid_hom.eval
modified theorem monoid_hom.eval_apply
modified theorem monoid_hom.ext
modified theorem monoid_hom.ext_iff
modified def monoid_hom.flip
modified theorem monoid_hom.flip_apply
modified def monoid_hom.id
modified theorem monoid_hom.id_apply
modified theorem monoid_hom.id_comp
modified theorem monoid_hom.injective_iff
modified theorem monoid_hom.inv_apply
modified theorem monoid_hom.inv_comp
modified theorem monoid_hom.map_mul
modified theorem monoid_hom.map_one
modified theorem monoid_hom.mk_coe
modified theorem monoid_hom.mul_apply
modified theorem monoid_hom.mul_comp
modified theorem monoid_hom.one_apply
modified theorem monoid_hom.one_comp
modified theorem monoid_hom.to_fun_eq_coe
modified theorem monoid_hom.to_mul_hom_coe
modified theorem monoid_hom.to_one_hom_coe
modified structure monoid_hom