Unbundled subfields (deprecated) #
This file is deprecated, and is no longer imported by anything in mathlib other than other deprecated files, and test files. You should not need to import it.
This file defines predicates for unbundled subfields. Instead of using this file, please use
Subfield, defined in
FieldTheory.Subfield, for subfields of fields.
Main definitions #
IsSubfield (S : Set F) is the predicate saying that a given subset of a field is
the set underlying a subfield. This structure is deprecated; use the bundled variant
Subfield F to model subfields of a field.