Commit 2020-09-22 12:57 516b0dfd

refactor(ring_theory/algebra): re-bundle subalgebra (#4180) 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.