Commit 2020-12-11 13:45 a372dfce

chore(*): don't assume sub_eq_add_neg and div_eq_mul_inv are defeq (#5302) This PR prepares for a follow-up PR (#5303) that adds div and sub fields to (add_)group(_with_zero). That follow-up 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. This preparation PR should have changed all places in mathlib that assumed defeqness, to rewrite explicitly instead. Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60div.60.20as.20a.20field.20in.20.60group(_with_zero).60