mathlib

5247d00f - feat(algebra/group_with_zero): add semigroup_with_zero (#7346)

feat(algebra/group_with_zero): add semigroup_with_zero (#7346) Split from #6786. By putting the new typeclass _before_ `mul_zero_one_class`, it doesn't need any annotations on `zero_ne_one` as the original PR did.