mathlib

78a9900b - refactor(algebra/group/hom_instances): relax semiring to non_unital_non_assoc_semiring in add_monoid_hom.mul (#11165)

refactor(algebra/group/hom_instances): relax semiring to non_unital_non_assoc_semiring in add_monoid_hom.mul (#11165) Previously `algebra.group.hom_instances` ended with some results showing that left and right multiplication operators are additive monoid homomorphisms between (unital, associative) semirings. The assumptions of a unit and associativity are not required for these results to work, so we relax the condition to `non_unital_non_assoc_semiring`. Required for #11073 .