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] - refactor(ring_theory/algebra): re-bundle subalgebra
#4180
Conversation
This PR makes `subalgebra` extend `subsemiring` instead of using `subsemiring` as a field in its definition. The refactor is needed because `intermediate_field` should simultaneously extend `subalgebra` and `subfield`, and so the type of the `carrier` fields should match. I added some copies of definitions that use `subring` instead of `is_subring` if I needed to change these definitions anyway.
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
bors d+
✌️ Vierkantor can now approve this pull request. To approve and merge a pull request, simply reply with |
…s_subring` Co-Authored-By: Floris van Doorn <fpvdoorn@gmail.com>
bors merge |
Canceled. |
Let's try that again: bors merge |
This PR makes `subalgebra` extend `subsemiring` instead of using `subsemiring` as a field in its definition. The refactor is needed because `intermediate_field` should simultaneously extend `subalgebra` and `subfield`, and so the type of the `carrier` fields should match. I added some copies of definitions that use `subring` instead of `is_subring` if I needed to change these definitions anyway.
Pull request successfully merged into master. Build succeeded: |
subalgebra
subalgebra
Define `intermediate_field K L` as a structure extending `subalgebra K L` and `subfield L`. This definition required some changes in `subalgebra`, which I added in #4180. Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>
Define `intermediate_field K L` as a structure extending `subalgebra K L` and `subfield L`. This definition required some changes in `subalgebra`, which I added in #4180. Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>
Define `intermediate_field K L` as a structure extending `subalgebra K L` and `subfield L`. This definition required some changes in `subalgebra`, which I added in #4180. Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>
This PR makes
subalgebra
extendsubsemiring
instead of usingsubsemiring
as a field in its definition. The refactor is needed becauseintermediate_field
should simultaneously extendsubalgebra
andsubfield
, and so the type of thecarrier
fields should match.I added some copies of definitions that use
subring
instead ofis_subring
if I needed to change these definitions anyway.