Unbundled subrings (deprecated) #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
ring_theory.subring.basic, for subrings of rings.
Main definitions #
is_subring (S : set R) : Prop : the predicate that
S is the underlying set of a subring
of the ring
R. The bundled variant
subring R should be used in preference to this.
- to_is_add_subgroup : is_add_subgroup S
- to_is_submonoid : is_submonoid S
S is a subring: a set containing 1 and closed under multiplication, addition and additive
The smallest subring containing a given subset of a ring, considered as a set. This function
is deprecated; use