Commit 2021-04-27 05:47 2d8ed1f5

chore(group_theory/eckmann_hilton): use mul_one_class and is_(left|right)_id (#7370) This ties these theorems slightly more to the rest of mathlib. The changes are:

• eckmann_hilton.comm_monoid now promotes a mul_one_class to a comm_monoid rather than taking two is_unital objects. This makes it consistent with eckmann_hilton.comm_group.
• is_unital is no longer a class, since it never had any instances and was never used as a typeclass argument.
• is_unital is now defined in terms of is_left_id and is_right_id.
• add_group.is_unital has been renamed to eckmann_hilton.add_zero_class.is_unital - the missing namespace was an accident, and the definition works much more generally than it was originally stated for.