mathlib3

cb7da1b4 - refactor(algebra/group/with_one): `inv_one_class` and related instances (#16697)

refactor(algebra/group/with_one): `inv_one_class` and related instances (#16697) Add instances for `neg_zero_class`, `inv_one_class` and `div_inv_one_monoid` for `with_zero`, and `inv_one_class` for `with_one`, under appropriate conditions.