mathlib3

1221ab6b - chore(*): add a `div`/`sub` field to (`add_`)`group`(`_with_zero`) (#5303)

chore(*): add a `div`/`sub` field to (`add_`)`group`(`_with_zero`) (#5303) This PR is intended to fix the following kind of diamonds: Let `foo X` be a type with a `∀ X, has_div (foo X)` instance but no `∀ X, has_inv (foo X)`, e.g. when `foo X` is a `euclidean_domain`. Suppose we also have an instance `∀ X [cromulent X], group_with_zero (foo X)`. Then the `(/)` coming from `group_with_zero_has_div` cannot be defeq to the `(/)` coming from `foo.has_div`. As a consequence of making the `has_div` instances defeq, we can no longer assume that `(div_eq_mul_inv a b : a / b = a * b⁻¹) = rfl` for all groups. The previous preparation PR #5302 should have changed all places in mathlib that assumed defeqness, to rewrite explicitly instead. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>