Commit 2020-12-11 13:45 a372dfce

View on Github →

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:

Estimated changes

added theorem div_left_injective
added theorem div_right_injective
added theorem group.inv_eq_one_div
added theorem group.mul_one_div
modified theorem neg_add'
deleted theorem sub_left_injective
deleted theorem sub_right_injective
modified theorem div_eq_inv_mul
deleted theorem div_eq_mul_inv
modified theorem div_one
modified theorem div_self
modified theorem one_div
modified theorem zero_div
modified theorem matrix.add_apply
modified theorem matrix.neg_apply
added theorem matrix.sub_apply
modified theorem matrix.zero_apply