Commit 2021-05-10 16:44 3417ee07

View on Github →

chore(deprecated/group): relax monoid to mul_one_class (#7556) This fixes an annoyance where monoid_hom.is_monoid_hom didn't work on non-associative monoids.

Estimated changes

Modified src/data/dfinsupp.lean

Modified src/deprecated/group.lean

modified theorem additive.is_add_monoid_hom

modified theorem is_monoid_hom.comp

modified theorem is_monoid_hom.of_mul

modified theorem multiplicative.is_monoid_hom