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: cleanups following #8609 and #8714 #8962
Conversation
Can you please fix the build error? |
Thanks! bors d+ |
✌️ alreadydone can now approve this pull request. To approve and merge a pull request, simply reply with |
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.
I addressed the reviews but also added more lemmas, so I'll wait for another approval or otherwise I'll merge tomorrow. Thanks!
It still looks good to me, thanks! |
bors merge |
+ generalize `image_rootSet`, `adjoin_rootSet_eq_range` and `splits_comp_of_splits` in Data/Polynomial/Splits and use the last one to golf `splits_of_algHom`, `splits_of_isScalarTower` (introduced in # 8609). + add three new lemmas `mem_range_x_of_minpoly_splits` to simplify the construction of `IntermediateField.algHomEquivAlgHomOfIsAlgClosed` and `Algebra.IsAlgebraic.algHomEquivAlgHomOfIsAlgClosed`, remove the `IsAlgClosed` condition and rename. ~~They could be moved to an earlier file but I refrain from doing that. (#find_home says it's already in the right place)~~ + golf `primitive_element_iff_algHom_eq_of_eval` from # 8609, using a new lemma `IsIntegral.minpoly_splits_tower_top` for the last step. + make `integralClosure_algEquiv_restrict` (from # 8714) computable and rename to `AlgEquiv.mapIntegralClosure` to follow camelCase naming convention and enable dot notation. Co-authored-by: Xavier-François Roblot <46200072+xroblot@users.noreply.github.com> Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
Pull request successfully merged into master. Build succeeded: |
+ generalize `image_rootSet`, `adjoin_rootSet_eq_range` and `splits_comp_of_splits` in Data/Polynomial/Splits and use the last one to golf `splits_of_algHom`, `splits_of_isScalarTower` (introduced in # 8609). + add three new lemmas `mem_range_x_of_minpoly_splits` to simplify the construction of `IntermediateField.algHomEquivAlgHomOfIsAlgClosed` and `Algebra.IsAlgebraic.algHomEquivAlgHomOfIsAlgClosed`, remove the `IsAlgClosed` condition and rename. ~~They could be moved to an earlier file but I refrain from doing that. (#find_home says it's already in the right place)~~ + golf `primitive_element_iff_algHom_eq_of_eval` from # 8609, using a new lemma `IsIntegral.minpoly_splits_tower_top` for the last step. + make `integralClosure_algEquiv_restrict` (from # 8714) computable and rename to `AlgEquiv.mapIntegralClosure` to follow camelCase naming convention and enable dot notation. Co-authored-by: Xavier-François Roblot <46200072+xroblot@users.noreply.github.com> Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
generalize
image_rootSet
,adjoin_rootSet_eq_range
andsplits_comp_of_splits
in Data/Polynomial/Splits and use the last one to golfsplits_of_algHom
,splits_of_isScalarTower
(introduced in # 8609).add three new lemmas
mem_range_x_of_minpoly_splits
to simplify the construction ofIntermediateField.algHomEquivAlgHomOfIsAlgClosed
andAlgebra.IsAlgebraic.algHomEquivAlgHomOfIsAlgClosed
, remove theIsAlgClosed
condition and rename.They could be moved to an earlier file but I refrain from doing that. (#find_home says it's already in the right place)golf
primitive_element_iff_algHom_eq_of_eval
from # 8609, using a new lemmaIsIntegral.minpoly_splits_tower_top
for the last step.make
integralClosure_algEquiv_restrict
(from # 8714) computable and rename toAlgEquiv.mapIntegralClosure
to follow camelCase naming convention and enable dot notation.