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.
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
[Merged by Bors] - feat: a polynomial over a perfect field is separable iff it is square-free #10170
Conversation
d7a107b
to
e9ce044
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM. The UFD proofs are on the longer side, but it sounds like there's an incoming refactor anyways, so I think we shouldn't spend too much energy on optimizing them.
bors d+
✌️ ocfnash can now approve this pull request. To approve and merge a pull request, simply reply with |
As this PR is labelled bors merge |
…-free (#10170) Yet another small step toward Jordan-Chevalley-Dunford. This was far more work than expected, partly because of missing API for `Squarefree`, and partly because the definition `IsCoprime` is the wrong concept for unique factorization domains.
Pull request successfully merged into master. Build succeeded: |
In fact this theorem admits a proof without using any lemmas introduced in #10170. For this I had to remove some redundant [GCDMonoid R] assumptions in RingTheory/PrincipalIdealDomain.lean. Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
In fact this theorem admits a proof without using any lemmas introduced in #10170. For this I had to remove some redundant [GCDMonoid R] assumptions in RingTheory/PrincipalIdealDomain.lean. Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
…-free (#10170) Yet another small step toward Jordan-Chevalley-Dunford. This was far more work than expected, partly because of missing API for `Squarefree`, and partly because the definition `IsCoprime` is the wrong concept for unique factorization domains.
In fact this theorem admits a proof without using any lemmas introduced in #10170. For this I had to remove some redundant [GCDMonoid R] assumptions in RingTheory/PrincipalIdealDomain.lean. Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
Yet another small step toward Jordan-Chevalley-Dunford.
This was far more work than expected, partly because of missing API for
Squarefree
, and partly because the definitionIsCoprime
is the wrong concept for unique factorization domains.