mathlib3

f92dc6c0 - feat(algebra/group_with_zero): non-associative monoid_with_zero (#7176)

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_hom`s 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`