[Merged by Bors] - feat(*): generalise+add algebraic instances #18947
Conversation
ericrbg
added
awaiting-review
github-actions
bot
added
the
modifies-synchronized-file
| { rat_cast := λ a, of f (a : K), | ||
| rat_cast_mk := λ a b h1 h2, | ||
| begin | ||
| letI : group_with_zero (adjoin_root f) := ideal.quotient.group_with_zero _, |
There was a problem hiding this comment.
This is a good compromise over what I pushed, thanks!
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
| -- seems to be causing a diamond in the below proof | ||
| -- however, this may be a fluke and the proof below uses non-canonical `algebra` instances: | ||
| -- when I replaced all the instances inside the proof with the "canonical" instances we have, | ||
| -- I had the (unprovable) goal (of the form) `adjoin_root.mk f (C x) = adjoin_root.mk f X` | ||
| -- for some `x, f`. So maybe this is indeed the correct approach and rewriting this proof is | ||
| -- salient in the future, or at least taking a closer look at the algebra instances it uses. | ||
| local attribute [-instance] adjoin_root.has_smul |
There was a problem hiding this comment.
Just to check, this still applies after the PR split?
There was a problem hiding this comment.
Yes, it was the issue that I had to merge this file over
There was a problem hiding this comment.
In #18952 I've completely removed the adjoin_root.has_smul instance. It works in this proof, let's see what CI thinks.
There was a problem hiding this comment.
CI seems to be happy, so maybe there is no need to add the has_smul instance manually?
There was a problem hiding this comment.
I think it's needed for the splitting_field stuff; I can try remove it there and see?
There was a problem hiding this comment.
I don't think removing it is any better than locally de-instancing. The proof happens to work because the instance priorities find the letI before the distrib_smul. We might in future find we need to deinstance the whole family of instances, and I don't think removing them makes sense
There was a problem hiding this comment.
LGTM, with some nits.
I think we should consider this blocked by some combination of
- The out-of-sync queue having overflowed a little
- Forward-porting @Hagb's PR first.
- My forward-port of the changes this used, [Merged by Bors] - chore: forward-port leanprover-community/mathlib#18934 mathlib4#3806
@Hagb, do you have time to update your forward-port PR (leanprover-community/mathlib4#3604), or do you need someone else to take over?
@eric-wieser Sorry for the delay. I had my conputer broken days ago, and I can update my PR before 2023-05-06 12:00 UTC (but maybe not now). |
github-actions
bot
removed
the
awaiting-CI
|
Actually, it seems that half of the slowdown of this lemma is not tactics, but actually elaboration |
2/3 of these have been resolved, and the out of sync queue is now at 10 - are we good to go? |
leanprover-community-bot-assistant
added
ready-to-merge
These are needed for #18857 (splitting field diamond), and I feel as though it's getting unwieldy so having these separately for review may be nice. Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
|
Don't forget to forward-port this! |
|
Is it possible to make port-dashboard make the author that changed things a sortable column? It'd be really good to have that |
|
You can type your name in the search box, which is almost as good. |
These are needed for #18857 (splitting field diamond), and I feel as though it's getting unwieldy so having these separately for review may be nice.