Skip to content
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.

Sign up for GitHub

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

Jump to bottom

feat(FieldTheory/Minpoly): minpoly K x splits implies minpoly K (algebraMap K L a - x) splits #17369

Open
wants to merge 204 commits into
base: master
Choose a base branch
from
Open

feat(FieldTheory/Minpoly): minpoly K x splits implies minpoly K (algebraMap K L a - x) splits #17369

wants to merge 204 commits into from
+136 −1

Conversation

jjdishere
Copy link
Collaborator

@jjdishere jjdishere commented Oct 2, 2024 •
edited by github-actions bot
Loading

Add minpoly K x splits implies minpoly K (- x) splits and minpoly K (algebraMap K L a - x) splits. This is after #17093 .

ericrbg and others added 30 commits July 21, 2023 18:44
@ericrbg
feat: refactor to use IsLocalRingHom more widely
d0ed84a
@ericrbg
tidy
41a78df
@ericrbg
fix
3bed6d4
@ericrbg
fix
18041da
@ericrbg
fix
f0e9e6e
@ericrbg
bump heartbeats - not super happy about this
5523b69
@ericrbg
move more stuff back
0d02fe2
@ericrbg
more technical fixes
0f3e600
@ericrbg
add another instance explicitly
836e4c0
@ericrbg
Merge remote-tracking branch 'origin/master' into ericrbg/local_ring_hom
7a2eb0b
@ericrbg @eric-wieser
style
668ffdb 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@ericrbg
Jireh's renaming
ecca48e
@ericrbg @j-loreaux
Update Mathlib/Algebra/Hom/Units.lean
98e9329 
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
@ericrbg
100char
1cfa845
@ericrbg
Merge remote-tracking branch 'origin/master' into ericrbg/local_ring_hom
0fbf224
@ericrbg
Merge remote-tracking branch 'origin/master' into ericrbg/local_ring_hom
7367e35
@ericrbg
rename
0778212
@ericrbg @eric-wieser
Update Mathlib/Algebra/GroupWithZero/Units/Basic.lean
5d7d0ba 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@ericrbg
Update Mathlib/Algebra/GroupWithZero/Units/Basic.lean
4f49cb9
@ericrbg
Merge branch 'master' into ericrbg/local_ring_hom
842354b
@ericrbg
update alias
fb6e9ca
@ericrbg
remove use of autoImplicit
f5c04bf
@ericrbg
more autoImplicit
9642033
@ericrbg
more autoImplicit
fdc3d39
@ericrbg
more autoImplicit
bc86def
@ericrbg
more autoImplicit
2bb6c58
@ericrbg
more autoImplicit
99198a1
@ericrbg
bump heartbeats
864a8d3
@ericrbg
tidy associated.lean
3358e8a
@ericrbg
speculative merge
780408c
@jjdishere jjdishere removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 21, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 22, 2024
@jjdishere jjdishere removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 23, 2024
alreadydone
alreadydone reviewed Oct 23, 2024
View reviewed changes
Mathlib/Algebra/Polynomial/AlgebraMap.lean Outdated Show resolved Hide resolved
Mathlib/Algebra/Polynomial/Splits.lean Outdated Show resolved Hide resolved
Mathlib/Algebra/Polynomial/Splits.lean Outdated Show resolved Hide resolved
alreadydone
alreadydone reviewed Oct 23, 2024
View reviewed changes
Copy link
Contributor

@alreadydone alreadydone left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For consistency:

Mathlib/Algebra/Polynomial/AlgebraMap.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/Adjoin/Field.lean Outdated Show resolved Hide resolved
jjdishere and others added 6 commits October 24, 2024 11:38
@jjdishere @alreadydone
Update Mathlib/Algebra/Polynomial/AlgebraMap.lean
47e9ef7 
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
@jjdishere @alreadydone
Update Mathlib/Algebra/Polynomial/Splits.lean
5a3697c 
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
@jjdishere @alreadydone
Update Mathlib/Algebra/Polynomial/AlgebraMap.lean
81a7c48 
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
@jjdishere @alreadydone
Update Mathlib/RingTheory/Adjoin/Field.lean
864d7cc 
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
@jjdishere
generalize to ax+b
120c9de
@jjdishere @github-actions
Update Mathlib/Algebra/Polynomial/AlgebraMap.lean
0174355 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@jjdishere jjdishere added the awaiting-author A reviewer has asked the author a question or requested changes label Oct 24, 2024
alreadydone
alreadydone reviewed Oct 25, 2024
View reviewed changes
Mathlib/Algebra/Polynomial/Splits.lean Outdated Show resolved Hide resolved
Mathlib/Algebra/Polynomial/AlgebraMap.lean Outdated Show resolved Hide resolved
Mathlib/Algebra/Polynomial/AlgebraMap.lean Outdated Show resolved Hide resolved
@jjdishere jjdishere mentioned this pull request Oct 25, 2024
Open
2 tasks
@jjdishere jjdishere removed the awaiting-author A reviewer has asked the author a question or requested changes label Oct 27, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 28, 2024
@jjdishere jjdishere removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 28, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@alreadydone alreadydone alreadydone left review comments

Assignees
No one assigned
Labels
blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) new-contributor This PR was made by a contributor with a most 5 merged PRs. Welcome to the community! t-algebra Algebra (groups, rings, fields, etc)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@jjdishere @mathlib4-dependent-issues-bot @alreadydone @leanprover-community-bot-assistant @ericrbg