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] - chore({ring_theory, field_theory}/*): fix imports to make #18021 less messy #18065
Conversation
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.
So if I read the changes correctly, apart from adjusting the imports, all other changes are moving the following definitions from ring_theory/adjoin_root.lean
to field_theory/minpoly/gcd_monoid.lean
:
minpoly.to_adjoin.injective
minpoly.equiv_adjoin
algebra.adjoin.power_basis'
power_basis.of_gen_mem_adjoin'
Could you add this information to the PR description, for future reference?
Looks good to me otherwise, thanks!
bors d+
✌️ Paul-Lez can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
bors r+ |
… messy (#18065) PR #18021 makes some changes to the theory of `minpoly`, which has the net effect that the structure of imports has to be changed for some files. This is a bit painful so I've decided to open a new PR instead of doing it in #18021. This PR also moves the following definitions from `ring_theory/adjoin_root.lean` to `field_theory/minpoly/gcd_monoid.lean`: - minpoly.to_adjoin.injective - minpoly.equiv_adjoin - algebra.adjoin.power_basis' - power_basis.of_gen_mem_adjoin' Co-authored-by: Paul Lezeau <paul.lezeau@gmail.com>
Pull request successfully merged into master. Build succeeded: |
PR #18021 makes some changes to the theory of
minpoly
, which has the net effect that the structure of imports has to be changed for some files. This is a bit painful so I've decided to open a new PR instead of doing it in #18021. This PR also moves the following definitions fromring_theory/adjoin_root.lean
tofield_theory/minpoly/gcd_monoid.lean
: