Unbundled subrings (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 subrings. Instead of using this file, please use
Subring, defined in
RingTheory.Subring.Basic, for subrings of rings.
Main definitions #