mathlib

48cc0c81 - feat(algebra/group_with_zero): groups with a zero element adjoined (#2242)

feat(algebra/group_with_zero): groups with a zero element adjoined (#2242) * feat(algebra/group_with_zero*): Basics on groups with a zero adjoined * feat(algebra/group_with_zero*): Basics on groups with a zero adjoined * Make argument implicit * Move inv_eq_zero out of gwz namespace * Partial refactor * Remove open_locale classical * Fix build * Factor out monoid_with_zero * Fix linter errors, hopefully * Fix build * Fix tests * Replace G with G0 * Add spaces around `^` * Add spaces and backticks in docstrings * Fix docstring of `mk0` * Fix statement of inv_eq_iff * Golf inv_injective * Golf inv_eq_zero * Remove the gwz namespace * Fix build Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>