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

[Merged by Bors] - feat(field_theory/separable): a separable polynomial is squarefree #5039

Closed
wants to merge 10 commits into from
Closed

[Merged by Bors] - feat(field_theory/separable): a separable polynomial is squarefree #5039

wants to merge 10 commits into from

Conversation

riccardobrasca
Copy link
Member

I prove that a separable polynomial is squarefree.

@riccardobrasca riccardobrasca added the awaiting-review The author would like community review of the PR label Nov 18, 2020
awainverse
awainverse reviewed Nov 18, 2020
View reviewed changes
src/field_theory/separable.lean
@@ -8,6 +8,7 @@ import algebra.polynomial.big_operators
import field_theory.minimal_polynomial
import field_theory.splitting_field
import field_theory.tower
import algebra.squarefree
Copy link
Collaborator

Choose a reason for hiding this comment

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

I made algebra.squarefree a pretty big import. It might be preferable to put this lemma on the file algebra.squarefree instead to accomodate that, idk.
(This is still fine with me, just wanted to make sure a maintainer checks this)

Copy link
Member Author

Choose a reason for hiding this comment

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

Ah yes, that's also possible. Just let me know which one is better.

Copy link
Member

Choose a reason for hiding this comment

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

I feel like this is the more natural location. Maybe we can minimize the imports in algebra.squarefree in a future PR.

@awainverse awainverse added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Nov 18, 2020
@riccardobrasca
Copy link
Member Author

What happens with number_theory/sum_two_squares?! CI has the same problem as in my other PR #5006... maybe it doesn't like me?

@riccardobrasca riccardobrasca added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Nov 18, 2020
@bryangingechen bryangingechen changed the title feat: (field_theory/separable): a separable polynomial is squarefree feat(field_theory/separable): a separable polynomial is squarefree Nov 18, 2020
@bryangingechen
Copy link
Collaborator

bryangingechen commented Nov 18, 2020 •
edited

What happens with number_theory/sum_two_squares?! CI has the same problem as in my other PR #5006... maybe it doesn't like me?

I haven't checked, but it could have to do with the fact that you added an import to field_theory/separable.lean; if this is in the transitive imports of number_theory/sum_two_squares, then something else named irreducible might show up and break the proof there.

@riccardobrasca
Copy link
Member Author

Yes, the problem is that Lean is trying to use nat.irreducible_iff_prime instead of principal_ideal_ring.irreducible_iff_prime. I do not know what I should do... modify number_theory/sum_two_squares?

pechersky
pechersky reviewed Nov 18, 2020
View reviewed changes
src/field_theory/separable.lean Outdated Show resolved Hide resolved
src/field_theory/separable.lean Outdated Show resolved Hide resolved
@fpvandoorn
Copy link
Member

fpvandoorn commented Nov 18, 2020 •
edited

In both PRs you add some imports so that the file sum_two_squares transitively imports ring_theory.int.basic, where nat.irreducible_iff_prime is declared. On current master, the file sum_two_squares doesn't know about nat.irreducible_iff_prime, so cannot get confused.

The best solution is to make sum_two_squares less ambiguous, for example by just writing out principal_ideal_ring.irreducible_iff_prime in full.

riccardobrasca and others added 5 commits November 18, 2020 23:32
@riccardobrasca @pechersky
Update src/field_theory/separable.lean
50fbfa4 
Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
@riccardobrasca @pechersky
Update src/field_theory/separable.lean
2a4e6d9 
Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
@riccardobrasca
Update separable.lean
d1836ea
@riccardobrasca
update number_theory/sum_two_squares
44a1c02
@riccardobrasca
Update separable.lean
235cfca
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Nov 19, 2020
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Nov 19, 2020
@jcommelin
Copy link
Member

Alternative: write open nat (hiding irreducible_iff_prime) in sum_two_squares.
(Instead of just open nat.)

But it is of course a bit more brittle, compared to Floris's suggestion.

@riccardobrasca
Copy link
Member Author

As you prefer, I put principal_ideal_ring.irreducible_iff_prime and is only a couple of lines longer.

@jcommelin
Copy link
Member

Ooh, just leave it like it is then. I just wanted to tell you about the other option 😃

@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Nov 19, 2020
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Nov 19, 2020
@fpvandoorn
Copy link
Member

Alternative: write open nat (hiding irreducible_iff_prime) in sum_two_squares.
(Instead of just open nat.)

But it is of course a bit more brittle, compared to Floris's suggestion.

The file only contains namespace nat, not open nat (that's why it's the default option: since the nat namespace is open, the name nat.irreducible_iff_prime takes priority over options in other namespaces)

@riccardobrasca
Copy link
Member Author

In any case this is now resolved since I merged my other PR #5006

@riccardobrasca riccardobrasca mentioned this pull request Nov 20, 2020
Closed
1 task
@awainverse
Copy link
Collaborator

LGTM

jcommelin
jcommelin approved these changes Nov 23, 2020
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

src/field_theory/separable.lean
@@ -8,6 +8,7 @@ import algebra.polynomial.big_operators
import field_theory.minimal_polynomial
import field_theory.splitting_field
import field_theory.tower
import algebra.squarefree
Copy link
Member

Choose a reason for hiding this comment

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

I feel like this is the more natural location. Maybe we can minimize the imports in algebra.squarefree in a future PR.

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Nov 23, 2020
bors bot pushed a commit that referenced this pull request Nov 23, 2020
@riccardobrasca
feat(field_theory/separable): a separable polynomial is squarefree (#…
562be70 
…5039)

I prove that a separable polynomial is squarefree.
@bors
Copy link

bors bot commented Nov 23, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(field_theory/separable): a separable polynomial is squarefree [Merged by Bors] - feat(field_theory/separable): a separable polynomial is squarefree Nov 23, 2020
@bors bors bot closed this Nov 23, 2020
@bors bors bot deleted the square_freee_sep branch November 23, 2020 15:20
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@pechersky pechersky pechersky left review comments

@fpvandoorn fpvandoorn fpvandoorn left review comments

@awainverse awainverse awainverse left review comments

@jcommelin jcommelin jcommelin approved these changes

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
6 participants
@riccardobrasca @bryangingechen @fpvandoorn @jcommelin @awainverse @pechersky