[Merged by Bors] - chore(*): add a div/sub field to (add_)group(_with_zero)
#5303
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Vierkantor
added
WIP
Vierkantor
force-pushed
the
sub_div_monoid
branch
2 times, most recently
from
0f9f524
to
fcaa620
Compare
github-actions
bot
added
the
merge-conflict
bors bot
pushed a commit
that referenced
this pull request
Dec 11, 2020
#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>
github-actions
bot
removed
the
blocked-by-other-PR
|
🎉 Great news! Looks like all the dependencies have been resolved: 💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
Vierkantor
force-pushed
the
sub_div_monoid
branch
from
fcaa620
to
459c4a8
Compare
github-actions
bot
removed
the
merge-conflict
Vierkantor
added
awaiting-review
|
There seem to be no obvious breakages in the low-level files, so let's see what CI thinks of the whole of mathlib... |
|
Does not build yet |
sgouezel
added
awaiting-author
Vierkantor
force-pushed
the
sub_div_monoid
branch
from
1c3a0da
to
cf9f89b
Compare
|
Now it compiles successfully on my machine. |
Vierkantor
added
awaiting-review
eric-wieser
reviewed
Dec 14, 2020
eric-wieser
reviewed
Dec 14, 2020
sgouezel
reviewed
Dec 14, 2020
I have added this as a comment on the declarations of |
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 commit should have changed all places in mathlib that assumed defeqness, to rewrite explicitly instead.
Vierkantor
force-pushed
the
sub_div_monoid
branch
from
64b594f
to
a58e124
Compare
(I could have sworn the line was just short enough; I cannot count apparently)
The elaborator managed to apply it by itself in a really messed-up way, so it looked like `norm_num` was unfolding stuff badly when really it was the elaborator a few lines previously
|
That was an epic refactor. Thanks a lot! 🎉 bors merge |
github-actions
bot
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Dec 16, 2020
…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>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
div/sub field to (add_)group(_with_zero)div/sub field to (add_)group(_with_zero)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR is intended to fix the following kind of diamonds:
Let
foo Xbe a type with a∀ X, has_div (foo X)instance but no∀ X, has_inv (foo X), e.g. whenfoo Xis aeuclidean_domain. Suppose we also have an instance∀ X [cromulent X], group_with_zero (foo X). Then the(/)coming fromgroup_with_zero_has_divcannot be defeq to the(/)coming fromfoo.has_div.As a consequence of making the
has_divinstances defeq, we can no longer assume that(div_eq_mul_inv a b : a / b = a * b⁻¹) = rflfor all groups. The previous preparation PR #5302 should have changed all places in mathlib that assumed defeqness, to rewrite explicitly instead.sub_eq_add_neganddiv_eq_mul_invare defeq #5302