Commit 2025-09-29 08:46 a9af4dc7

feat(Algebra/Group/Hom/Defs): MonoidHom switching from MulOneClass to MulOne (#28702) Currently MonoidHom relies on a MulOneClass, stating that 1 is a multiplicative identity; when actually all a "monoid" hom does is preserve multiplication and one. So, really, a MonoidHom is a "mul-and-one hom", but one cannot use it with any type that isn't a MulOneClass. (It also does not enforce being a Monoid: associativity is not required.) In general, homs like this should only rely on the data being present in the source and destination type; any applications of it are then free to assume MulOneClass or Monoid where appropriate, which is essentially already how it does. This drops the MulOneClass assumption so that MonoidHom just takes the Mul and One types. But if we wrote MonoidHom [Mul M] [One M], this would essentially double the effort needed for typeclass inference. An experiment in #28889 confirmed this performance hit. So, we define a MulOne type which is just the Mul and One data bundled together, and the performance change becomes pretty minimal. And then there are the corresponding changes to AddMonoidHom / AddZeroClass becoming AddZero. This follows some discussion at #mathlib4 > RingHom for not-a-ring