mathlib3

2d8ed1f5 - chore(group_theory/eckmann_hilton): use `mul_one_class` and `is_(left|right)_id` (#7370)

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.