-
Notifications
You must be signed in to change notification settings - Fork 297
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(linear_algebra/annihilating_polynomial): add definition of annihilating ideal and show minpoly generates in field case #12140
Conversation
@eric-wieser just following up. Anything else needed on this? |
14a096c
to
f511cb2
Compare
4ecd8aa
to
ca686aa
Compare
Can you please merge master to see if this still works? |
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.
Sorry for the wait, I only just got time to get around to all the reviews. There are still some (relatively minor) comments in annihilating_polynomial.lean
that you haven't addressed. Could you merge master and address them?
bors merge |
…ilating ideal and show minpoly generates in field case (#12140) adding item from trivial undergrad subjects list Co-authored-by: Patrick Massot <patrickmassot@free.fr> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
Build failed (retrying...): |
…ilating ideal and show minpoly generates in field case (#12140) adding item from trivial undergrad subjects list Co-authored-by: Patrick Massot <patrickmassot@free.fr> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
Build failed: |
I think this needs a master merge |
…ilating ideal and show minpoly generates in field case
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
fc2b45d
to
2a51c00
Compare
bors merge |
…ilating ideal and show minpoly generates in field case (#12140) adding item from trivial undergrad subjects list Co-authored-by: Patrick Massot <patrickmassot@free.fr> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
Pull request successfully merged into master. Build succeeded: |
…ilating ideal and show minpoly generates in field case (leanprover-community#12140) adding item from trivial undergrad subjects list Co-authored-by: Patrick Massot <patrickmassot@free.fr> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
…ilating ideal and show minpoly generates in field case (#12140) adding item from trivial undergrad subjects list Co-authored-by: Patrick Massot <patrickmassot@free.fr> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
…ilating ideal and show minpoly generates in field case (#12140) adding item from trivial undergrad subjects list Co-authored-by: Patrick Massot <patrickmassot@free.fr> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
adding item from trivial undergrad subjects list