-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore(*): don't assume sub_eq_add_neg
and div_eq_mul_inv
are defeq
#5302
Conversation
This commit prepares for a follow-up that makes `div` and `sub` fields in (`add_`)`group`(`_with_zero`).
(Because fields don't extend `div_inv_monoid` yet.)
Since the PR is still getting errors, I'm marking it as WIP until it compiles again. |
I have fixed |
Great, thank you so much! |
The linter complains. I'll let you fix it, then I'll review your changes (and you will have to review mine!) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Your changes LGTM otherwise 👍
Let's merge this. Thanks a lot! |
#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 Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Pull request successfully merged into master. Build succeeded: |
sub_eq_add_neg
and div_eq_mul_inv
are defeqsub_eq_add_neg
and div_eq_mul_inv
are defeq
…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>
This PR prepares for a follow-up PR (#5303) that adds
div
andsub
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. whenfoo X
is aeuclidean_domain
. Suppose we also have an instance∀ X [cromulent X], group_with_zero (foo X)
. Then the(/)
coming fromgroup_with_zero_has_div
cannot be defeq to the(/)
coming fromfoo.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