mathlib
516b0dfd - refactor(ring_theory/algebra): re-bundle `subalgebra` (#4180)

Commit
5 years ago
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.
Author
Parents
Loading