[Merged by Bors] - feat: port FieldTheory.SplittingField.Construction #4891
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
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
ChrisHughes24
added
mathlib-port
|
@ChrisHughes24 in case you forgot, there may be fixes in #4339 that can be salvaged |
I didn't forget. I'm going to claim this for about a day I think. I have an idea about how to tidy it up a lot. |
ChrisHughes24
added
help-wanted
3 tasks
eric-wieser
reviewed
Jun 12, 2023
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
jcommelin
added
the
awaiting-review
|
LGTM. |
|
Maybe we should add a co authored by because I stole code from the previous PR. |
|
Should we wait to fix the mathlib3 problems before merging this? The relevant PR is #19178. |
|
I think we should also forward-port #19179 first. The version of those changes in this PR is not identical to the ones in mathlib3, and a forward-port PR would create an easy place to align them |
semorrison
added
the
blocked-by-other-PR
semorrison
removed
the
blocked-by-other-PR
|
This PR/issue depends on: |
bors bot
pushed a commit
to leanprover-community/mathlib
that referenced
this pull request
Jun 15, 2023
We refactor the definition of `splitting_field`. The main motivation is to backport [!4#4891](leanprover-community/mathlib4#4891) since the is seems very problematic to port the current design. Zulip discussion relevant to this PR: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.234891.20.20FieldTheory.2ESplittingField
|
Now that Lean 3 is happy with the corresponding refactor, let's get this merged! |
|
bors r+ |
github-actions
bot
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Jun 15, 2023
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Eric Wieser <wieser.eric@gmail.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
eric-wieser
reviewed
Jun 15, 2023
Comment on lines
+153
to
+159
| --Porting note: new instance | ||
| instance isScalarTower_right [CommSemiring R] [CommSemiring S₁] [DistribSMul R S₁] | ||
| [IsScalarTower R S₁ S₁] : IsScalarTower R (MvPolynomial σ S₁) (MvPolynomial σ S₁) := | ||
| ⟨by | ||
| rintro x p q | ||
| dsimp [MvPolynomial] at p q ⊢ | ||
| rw [smul_mul_assoc]⟩ |
bors bot
pushed a commit
that referenced
this pull request
Jun 15, 2023
A sloppy version of this was added in #4891. This adds the better version that we wrote in mathlib3.
alexkeizer
pushed a commit
that referenced
this pull request
Jun 22, 2023
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
alexkeizer
pushed a commit
that referenced
this pull request
Jun 22, 2023
A sloppy version of this was added in #4891. This adds the better version that we wrote in mathlib3.
semorrison
pushed a commit
that referenced
this pull request
Jun 25, 2023
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
semorrison
pushed a commit
that referenced
this pull request
Jun 25, 2023
A sloppy version of this was added in #4891. This adds the better version that we wrote in mathlib3.
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.
I've started a slightly different approach to this PR. So far I've constructed a
SplittingFieldAuxwithout worrying about whether the instances satisfy nice definitional equalities. Then the actualSplittingFieldis defined to be a quotient of anMvPolynomialring by the kernel of the obvious map intoSplittingFieldAux. Because the actualSplittingFieldwill be a quotient of aMvPolynomialit should have nice instances on it.This is just a suggestion, if somebody prefers doing it the old way and reviving the old PR, I won't object to that.