Mathlib v3 is deprecated. Go to Mathlib v4

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 theorem monoid_hom.coe_prod
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
modified def add_monoid_hom.single
modified def monoid_hom.coe_fn
modified theorem pi.single_add
modified theorem prod.fst_mul_snd
modified theorem with_one.map_comp
modified def add_monoid_algebra.of
modified theorem add_monoid_algebra.of_apply
modified theorem monoid_algebra.lift_nc_smul
modified theorem monoid_algebra.of_apply
modified theorem monoid_algebra.of_injective
modified theorem dfinsupp.add_apply
modified theorem dfinsupp.add_hom_ext'
modified theorem dfinsupp.add_hom_ext
modified theorem dfinsupp.coe_add
modified theorem dfinsupp.comp_lift_add_hom
modified theorem dfinsupp.comp_sum_add_hom
modified def dfinsupp.lift_add_hom
modified theorem dfinsupp.mk_add
modified theorem dfinsupp.subtype_domain_add
modified def dfinsupp.sum_add_hom
modified theorem dfinsupp.sum_add_hom_add
modified theorem dfinsupp.sum_add_hom_apply
modified theorem dfinsupp.sum_add_hom_single
modified theorem dfinsupp.sum_add_hom_zero
modified theorem dfinsupp.support_add
modified theorem monoid_hom.coe_to_mul_equiv
modified def mul_equiv.arrow_congr
modified theorem mul_equiv.coe_to_monoid_hom
modified theorem mul_equiv.map_eq_one_iff
modified theorem mul_equiv.map_ne_one_iff
modified theorem mul_equiv.map_one
modified def mul_equiv.to_additive
modified theorem finsupp.add_hom_ext'
modified theorem finsupp.add_hom_ext
modified theorem finsupp.map_range_add
modified theorem finsupp.mul_hom_ext'
modified theorem finsupp.mul_hom_ext
modified def set.mul_indicator_hom
modified structure add_submonoid
modified def monoid_hom.of_mdense
modified structure submonoid
modified theorem submonoid.mem_powers
modified def submonoid.powers
modified theorem submonoid.powers_eq_closure
modified theorem submonoid.powers_subset
modified def monoid_hom.mrestrict
modified theorem monoid_hom.mrestrict_apply