Commit 2020-12-16 15:31 1221ab6b

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.