-
Notifications
You must be signed in to change notification settings - Fork 298
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(field_theory/splitting_field): remove unneeded parameter #15716
Conversation
The definition of `splitting_field_aux` relied on a parameter `hfn : n = f.nat_degree` that was never actually used in the construction or its instances, only in the `splits` theorem. So we might as well delete it. This PR prepares for a redefinition of all instances on `splitting_field_aux` to fix instance diamonds, see the `splitting_field-diamond` branch for progress.
bors d+ This all looks reasonable to me. I guess one thing to consider is whether it should be called |
✌️ Vierkantor can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
The definition of `splitting_field_aux` relied on a parameter `hfn : n = f.nat_degree` that was never actually used in the construction or its instances, only in the `splits` theorem. So we might as well delete it. This PR prepares for a redefinition of all instances on `splitting_field_aux` to fix instance diamonds, see the `splitting_field-diamond` branch for progress. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
bors merge |
The definition of `splitting_field_aux` relied on a parameter `hfn : n = f.nat_degree` that was never actually used in the construction or its instances, only in the `splits` theorem. So we might as well delete it. This PR prepares for a redefinition of all instances on `splitting_field_aux` to fix instance diamonds, see the `splitting_field-diamond` branch for progress. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
…rover-community#15716) The definition of `splitting_field_aux` relied on a parameter `hfn : n = f.nat_degree` that was never actually used in the construction or its instances, only in the `splits` theorem. So we might as well delete it. This PR prepares for a redefinition of all instances on `splitting_field_aux` to fix instance diamonds, see the `splitting_field-diamond` branch for progress. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
The definition of `splitting_field_aux` relied on a parameter `hfn : n = f.nat_degree` that was never actually used in the construction or its instances, only in the `splits` theorem. So we might as well delete it. This PR prepares for a redefinition of all instances on `splitting_field_aux` to fix instance diamonds, see the `splitting_field-diamond` branch for progress. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
The definition of `splitting_field_aux` relied on a parameter `hfn : n = f.nat_degree` that was never actually used in the construction or its instances, only in the `splits` theorem. So we might as well delete it. This PR prepares for a redefinition of all instances on `splitting_field_aux` to fix instance diamonds, see the `splitting_field-diamond` branch for progress. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
The definition of
splitting_field_aux
relied on a parameterhfn : n = f.nat_degree
that was never actually used in the construction or its instances, only in thesplits
theorem. So we might as well delete it.This PR prepares for a redefinition of all instances on
splitting_field_aux
to fix instance diamonds, see thesplitting_field-diamond
branch for progress.