Commit 2021-04-15 15:46 f92dc6c0

feat(algebra/group_with_zero): non-associative monoid_with_zero (#7176) This introduces a new mul_zero_one_class which is monoid_with_zero without associativity, just as mul_one_class is monoid without associativity. This would help expand the scope of #6786 to include ring_homs, something that was previously blocked by monoid_with_zero and the non_assoc_semiring having no common ancestor with 0, 1, and *. Using #6865 as a template for what to cover, this PR includes;

• Generalizing monoid_with_zero_hom to require the weaker mul_zero_one_class. This has a slight downside, in that some_mwzh.to_monoid_hom now holds as its typeclass argument mul_zero_one_class.to_mul_one_class instead of monoid_with_zero.to_monoid. This means that lemmas about monoid_homs with associate multiplication no longer always elaborate correctly without type annotations, as the monoid instance has to be found by typeclass search instead of unification.
• function.(in|sur)jective.mul_zero_one_class
• equiv.mul_zero_one_class
• Adding instances for:
  • prod
  • pi
  • set_semiring
  • with_zero
  • locally_constant
  • monoid_algebra
  • add_monoid_algebra