mathlib3

169bb29d - feat(algebra/group/with_one): cleanup algebraic instances (#10194)

feat(algebra/group/with_one): cleanup algebraic instances (#10194) This: * adds a `has_neg (with_zero α)` instance which sends `0` to `0` and otherwise uses the underlying negation (and the same for `has_inv (with_one α)`). * replaces the `has_div (with_zero α)`, `has_pow (with_zero α) ℕ`, and `has_pow (with_zero α) ℤ` instances in order to produce better definitional properties than the previous default ones.