Commit 2021-11-06 20:27 169bb29d

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.