mathlib3
3417ee07 - chore(deprecated/group): relax monoid to mul_one_class (#7556)

Commit

4 years ago

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.

Author

eric-wieser

Parents

477af65c

mathlib3 3417ee07 - chore(deprecated/group): relax monoid to mul_one_class (#7556)

mathlib3
3417ee07 - chore(deprecated/group): relax monoid to mul_one_class (#7556)