refactor(field-theory/subfield): bundled subfields (#4159)
Define bundled subfields. The contents of the new `subfield` file are basically a copy of `subring.lean` with the replacement `subring` -> `subfield`, and the proofs repaired as necessary.
As with the other bundled subobject refactors, other files depending on unbundled subfields now import `deprecated.subfield`.
Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>
