# mathlibdocumentation

ring_theory.subring.basic

# Subrings #

Let `R` be a ring. This file defines the "bundled" subring type `subring R`, a type whose terms correspond to subrings of `R`. This is the preferred way to talk about subrings in mathlib. Unbundled subrings (`s : set R` and `is_subring s`) are not in this file, and they will ultimately be deprecated.

We prove that subrings are a complete lattice, and that you can `map` (pushforward) and `comap` (pull back) them along ring homomorphisms.

We define the `closure` construction from `set R` to `subring R`, sending a subset of `R` to the subring it generates, and prove that it is a Galois insertion.

## Main definitions #

Notation used here:

`(R : Type u) [ring R] (S : Type u) [ring S] (f g : R →+* S)` `(A : subring R) (B : subring S) (s : set R)`

• `subring R` : the type of subrings of a ring `R`.

• `instance : complete_lattice (subring R)` : the complete lattice structure on the subrings.

• `subring.center` : the center of a ring `R`.

• `subring.closure` : subring closure of a set, i.e., the smallest subring that includes the set.

• `subring.gi` : `closure : set M → subring M` and coercion `coe : subring M → set M` form a `galois_insertion`.

• `comap f B : subring A` : the preimage of a subring `B` along the ring homomorphism `f`

• `map f A : subring B` : the image of a subring `A` along the ring homomorphism `f`.

• `prod A B : subring (R × S)` : the product of subrings

• `f.range : subring B` : the range of the ring homomorphism `f`.

• `eq_locus f g : subring R` : given ring homomorphisms `f g : R →+* S`, the subring of `R` where `f x = g x`

## Implementation notes #

A subring is implemented as a subsemiring which is also an additive subgroup. The initial PR was as a submonoid which is also an additive subgroup.

Lattice inclusion (e.g. `≤` and `⊓`) is used rather than set notation (`⊆` and `∩`), although `∈` is defined as membership of a subring's underlying set.

## Tags #

subring, subrings

@[class]
structure subring_class (S : Type u_1) (R : out_param (Type u)) [ring R] [ R] :
Type
• to_subsemiring_class :
• neg_mem : ∀ {s : S} {a : R}, a s-a s

`subring_class S R` states that `S` is a type of subsets `s ⊆ R` that are both a multiplicative submonoid and an additive subgroup.

Instances of this typeclass
Instances of other typeclasses for `subring_class`
• subring_class.has_sizeof_inst
@[protected, instance]
def subring_class.add_subgroup_class (S : Type u_1) (R : out_param (Type u)) [ R] [ring R] [h : R] :
Equations
theorem coe_int_mem {R : Type u} {S : Type v} [ring R] [ R] [hSR : R] (s : S) (n : ) :
n s
@[protected, instance]
def subring_class.to_has_int_cast {R : Type u} {S : Type v} [ring R] [ R] [hSR : R] (s : S) :
Equations
@[protected, instance]
def subring_class.to_ring {R : Type u} {S : Type v} [ring R] [ R] [hSR : R] (s : S) :

A subring of a ring inherits a ring structure

Equations
• = _ _ _ _ _ _ _ _ _
@[protected, instance]
def subring_class.to_comm_ring {S : Type v} (s : S) {R : Type u_1} [comm_ring R] [ R] [ R] :

A subring of a `comm_ring` is a `comm_ring`.

Equations
• = _ _ _ _ _ _ _ _ _
@[protected, instance]
def subring_class.is_domain {S : Type v} (s : S) {R : Type u_1} [ring R] [is_domain R] [ R] [ R] :

A subring of a domain is a domain.

@[protected, instance]
def subring_class.to_ordered_ring {S : Type v} (s : S) {R : Type u_1} [ordered_ring R] [ R] [ R] :

A subring of an `ordered_ring` is an `ordered_ring`.

Equations
• = _ _ _ _ _ _ _ _
@[protected, instance]
def subring_class.to_ordered_comm_ring {S : Type v} (s : S) {R : Type u_1} [ R] [ R] :

A subring of an `ordered_comm_ring` is an `ordered_comm_ring`.

Equations
• = _ _ _ _ _ _ _ _
@[protected, instance]
def subring_class.to_linear_ordered_ring {S : Type v} (s : S) {R : Type u_1} [ R] [ R] :

A subring of a `linear_ordered_ring` is a `linear_ordered_ring`.

Equations
• = _ _ _ _ _ _ _
@[protected, instance]
def subring_class.to_linear_ordered_comm_ring {S : Type v} (s : S) {R : Type u_1} [ R] [ R] :

A subring of a `linear_ordered_comm_ring` is a `linear_ordered_comm_ring`.

Equations
• = _ _ _ _ _ _ _
def subring_class.subtype {R : Type u} {S : Type v} [ring R] [ R] [hSR : R] (s : S) :

The natural ring hom from a subring of ring `R` to `R`.

Equations
@[simp]
theorem subring_class.coe_subtype {R : Type u} {S : Type v} [ring R] [ R] [hSR : R] (s : S) :
@[simp, norm_cast]
theorem subring_class.coe_nat_cast {R : Type u} {S : Type v} [ring R] [ R] [hSR : R] (s : S) (n : ) :
@[simp, norm_cast]
theorem subring_class.coe_int_cast {R : Type u} {S : Type v} [ring R] [ R] [hSR : R] (s : S) (n : ) :
def subring.to_add_subgroup {R : Type u} [ring R] (self : subring R) :

Reinterpret a `subring` as an `add_subgroup`.

structure subring (R : Type u) [ring R] :
Type u

`subring R` is the type of subrings of `R`. A subring of `R` is a subset `s` that is a multiplicative submonoid and an additive subgroup. Note in particular that it shares the same 0 and 1 as R.

Instances for `subring`
def subring.to_subsemiring {R : Type u} [ring R] (self : subring R) :

Reinterpret a `subring` as a `subsemiring`.

def subring.to_submonoid {R : Type u} [ring R] (s : subring R) :

The underlying submonoid of a subring.

Equations
@[protected, instance]
def subring.set_like {R : Type u} [ring R] :
Equations
@[protected, instance]
def subring.subring_class {R : Type u} [ring R] :
R
Equations
@[simp]
theorem subring.mem_carrier {R : Type u} [ring R] {s : subring R} {x : R} :
x s.carrier x s
@[simp]
theorem subring.mem_mk {R : Type u} [ring R] {S : set R} {x : R} (h₁ : ∀ {a b : R}, a Sb Sa * b S) (h₂ : 1 S) (h₃ : ∀ {a b : R}, a Sb Sa + b S) (h₄ : 0 S) (h₅ : ∀ {x : R}, x S-x S) :
x {carrier := S, mul_mem' := h₁, one_mem' := h₂, add_mem' := h₃, zero_mem' := h₄, neg_mem' := h₅} x S
@[simp]
theorem subring.coe_set_mk {R : Type u} [ring R] (S : set R) (h₁ : ∀ {a b : R}, a Sb Sa * b S) (h₂ : 1 S) (h₃ : ∀ {a b : R}, a Sb Sa + b S) (h₄ : 0 S) (h₅ : ∀ {x : R}, x S-x S) :
{carrier := S, mul_mem' := h₁, one_mem' := h₂, add_mem' := h₃, zero_mem' := h₄, neg_mem' := h₅} = S
@[simp]
theorem subring.mk_le_mk {R : Type u} [ring R] {S S' : set R} (h₁ : ∀ {a b : R}, a Sb Sa * b S) (h₂ : 1 S) (h₃ : ∀ {a b : R}, a Sb Sa + b S) (h₄ : 0 S) (h₅ : ∀ {x : R}, x S-x S) (h₁' : ∀ {a b : R}, a S'b S'a * b S') (h₂' : 1 S') (h₃' : ∀ {a b : R}, a S'b S'a + b S') (h₄' : 0 S') (h₅' : ∀ {x : R}, x S'-x S') :
{carrier := S, mul_mem' := h₁, one_mem' := h₂, add_mem' := h₃, zero_mem' := h₄, neg_mem' := h₅} {carrier := S', mul_mem' := h₁', one_mem' := h₂', add_mem' := h₃', zero_mem' := h₄', neg_mem' := h₅'} S S'
@[ext]
theorem subring.ext {R : Type u} [ring R] {S T : subring R} (h : ∀ (x : R), x S x T) :
S = T

Two subrings are equal if they have the same elements.

@[protected]
def subring.copy {R : Type u} [ring R] (S : subring R) (s : set R) (hs : s = S) :

Copy of a subring with a new `carrier` equal to the old one. Useful to fix definitional equalities.

Equations
@[simp]
theorem subring.coe_copy {R : Type u} [ring R] (S : subring R) (s : set R) (hs : s = S) :
(S.copy s hs) = s
theorem subring.copy_eq {R : Type u} [ring R] (S : subring R) (s : set R) (hs : s = S) :
S.copy s hs = S
theorem subring.to_subsemiring_injective {R : Type u} [ring R] :
theorem subring.to_subsemiring_strict_mono {R : Type u} [ring R] :
theorem subring.to_subsemiring_mono {R : Type u} [ring R] :
theorem subring.to_add_subgroup_injective {R : Type u} [ring R] :
theorem subring.to_add_subgroup_strict_mono {R : Type u} [ring R] :
theorem subring.to_add_subgroup_mono {R : Type u} [ring R] :
theorem subring.to_submonoid_injective {R : Type u} [ring R] :
theorem subring.to_submonoid_strict_mono {R : Type u} [ring R] :
theorem subring.to_submonoid_mono {R : Type u} [ring R] :
@[protected]
def subring.mk' {R : Type u} [ring R] (s : set R) (sm : submonoid R) (sa : add_subgroup R) (hm : sm = s) (ha : sa = s) :

Construct a `subring R` from a set `s`, a submonoid `sm`, and an additive subgroup `sa` such that `x ∈ s ↔ x ∈ sm ↔ x ∈ sa`.

Equations
@[simp]
theorem subring.coe_mk' {R : Type u} [ring R] {s : set R} {sm : submonoid R} (hm : sm = s) {sa : add_subgroup R} (ha : sa = s) :
sm sa hm ha) = s
@[simp]
theorem subring.mem_mk' {R : Type u} [ring R] {s : set R} {sm : submonoid R} (hm : sm = s) {sa : add_subgroup R} (ha : sa = s) {x : R} :
x sm sa hm ha x s
@[simp]
theorem subring.mk'_to_submonoid {R : Type u} [ring R] {s : set R} {sm : submonoid R} (hm : sm = s) {sa : add_subgroup R} (ha : sa = s) :
sm sa hm ha).to_submonoid = sm
@[simp]
theorem subring.mk'_to_add_subgroup {R : Type u} [ring R] {s : set R} {sm : submonoid R} (hm : sm = s) {sa : add_subgroup R} (ha : sa = s) :
sm sa hm ha).to_add_subgroup = sa
def subsemiring.to_subring {R : Type u} [ring R] (s : subsemiring R) (hneg : -1 s) :

A `subsemiring` containing -1 is a `subring`.

Equations
@[protected]
theorem subring.one_mem {R : Type u} [ring R] (s : subring R) :
1 s

A subring contains the ring's 1.

@[protected]
theorem subring.zero_mem {R : Type u} [ring R] (s : subring R) :
0 s

A subring contains the ring's 0.

@[protected]
theorem subring.mul_mem {R : Type u} [ring R] (s : subring R) {x y : R} :
x sy sx * y s

A subring is closed under multiplication.

@[protected]
theorem subring.add_mem {R : Type u} [ring R] (s : subring R) {x y : R} :
x sy sx + y s

A subring is closed under addition.

@[protected]
theorem subring.neg_mem {R : Type u} [ring R] (s : subring R) {x : R} :
x s-x s

A subring is closed under negation.

@[protected]
theorem subring.sub_mem {R : Type u} [ring R] (s : subring R) {x y : R} (hx : x s) (hy : y s) :
x - y s

A subring is closed under subtraction

@[protected]
theorem subring.list_prod_mem {R : Type u} [ring R] (s : subring R) {l : list R} :
(∀ (x : R), x lx s)l.prod s

Product of a list of elements in a subring is in the subring.

@[protected]
theorem subring.list_sum_mem {R : Type u} [ring R] (s : subring R) {l : list R} :
(∀ (x : R), x lx s)l.sum s

Sum of a list of elements in a subring is in the subring.

@[protected]
theorem subring.multiset_prod_mem {R : Type u_1} [comm_ring R] (s : subring R) (m : multiset R) :
(∀ (a : R), a ma s)m.prod s

Product of a multiset of elements in a subring of a `comm_ring` is in the subring.

@[protected]
theorem subring.multiset_sum_mem {R : Type u_1} [ring R] (s : subring R) (m : multiset R) :
(∀ (a : R), a ma s)m.sum s

Sum of a multiset of elements in an `subring` of a `ring` is in the `subring`.

@[protected]
theorem subring.prod_mem {R : Type u_1} [comm_ring R] (s : subring R) {ι : Type u_2} {t : finset ι} {f : ι → R} (h : ∀ (c : ι), c tf c s) :
t.prod (λ (i : ι), f i) s

Product of elements of a subring of a `comm_ring` indexed by a `finset` is in the subring.

@[protected]
theorem subring.sum_mem {R : Type u_1} [ring R] (s : subring R) {ι : Type u_2} {t : finset ι} {f : ι → R} (h : ∀ (c : ι), c tf c s) :
t.sum (λ (i : ι), f i) s

Sum of elements in a `subring` of a `ring` indexed by a `finset` is in the `subring`.

@[protected, instance]
def subring.to_ring {R : Type u} [ring R] (s : subring R) :

A subring of a ring inherits a ring structure

Equations
@[protected]
theorem subring.zsmul_mem {R : Type u} [ring R] (s : subring R) {x : R} (hx : x s) (n : ) :
n x s
@[protected]
theorem subring.pow_mem {R : Type u} [ring R] (s : subring R) {x : R} (hx : x s) (n : ) :
x ^ n s
@[simp, norm_cast]
theorem subring.coe_add {R : Type u} [ring R] (s : subring R) (x y : s) :
(x + y) = x + y
@[simp, norm_cast]
theorem subring.coe_neg {R : Type u} [ring R] (s : subring R) (x : s) :
@[simp, norm_cast]
theorem subring.coe_mul {R : Type u} [ring R] (s : subring R) (x y : s) :
(x * y) = x * y
@[simp, norm_cast]
theorem subring.coe_zero {R : Type u} [ring R] (s : subring R) :
0 = 0
@[simp, norm_cast]
theorem subring.coe_one {R : Type u} [ring R] (s : subring R) :
1 = 1
@[simp, norm_cast]
theorem subring.coe_pow {R : Type u} [ring R] (s : subring R) (x : s) (n : ) :
(x ^ n) = x ^ n
@[simp]
theorem subring.coe_eq_zero_iff {R : Type u} [ring R] (s : subring R) {x : s} :
x = 0 x = 0
@[protected, instance]
def subring.to_comm_ring {R : Type u_1} [comm_ring R] (s : subring R) :

A subring of a `comm_ring` is a `comm_ring`.

Equations
@[protected, instance]
def subring.nontrivial {R : Type u_1} [ring R] [nontrivial R] (s : subring R) :

A subring of a non-trivial ring is non-trivial.

@[protected, instance]
def subring.no_zero_divisors {R : Type u_1} [ring R] (s : subring R) :

A subring of a ring with no zero divisors has no zero divisors.

@[protected, instance]
def subring.is_domain {R : Type u_1} [ring R] [is_domain R] (s : subring R) :

A subring of a domain is a domain.

@[protected, instance]
def subring.to_ordered_ring {R : Type u_1} [ordered_ring R] (s : subring R) :

A subring of an `ordered_ring` is an `ordered_ring`.

Equations
@[protected, instance]
def subring.to_ordered_comm_ring {R : Type u_1} (s : subring R) :

A subring of an `ordered_comm_ring` is an `ordered_comm_ring`.

Equations
@[protected, instance]
def subring.to_linear_ordered_ring {R : Type u_1} (s : subring R) :

A subring of a `linear_ordered_ring` is a `linear_ordered_ring`.

Equations
@[protected, instance]
def subring.to_linear_ordered_comm_ring {R : Type u_1} (s : subring R) :

A subring of a `linear_ordered_comm_ring` is a `linear_ordered_comm_ring`.

Equations
def subring.subtype {R : Type u} [ring R] (s : subring R) :

The natural ring hom from a subring of ring `R` to `R`.

Equations
@[simp]
theorem subring.coe_subtype {R : Type u} [ring R] (s : subring R) :
@[simp, norm_cast]
theorem subring.coe_nat_cast {R : Type u} [ring R] (s : subring R) (n : ) :
@[simp, norm_cast]
theorem subring.coe_int_cast {R : Type u} [ring R] (s : subring R) (n : ) :

## Partial order #

@[simp]
theorem subring.mem_to_submonoid {R : Type u} [ring R] {s : subring R} {x : R} :
x s
@[simp]
theorem subring.coe_to_submonoid {R : Type u} [ring R] (s : subring R) :
@[simp]
theorem subring.mem_to_add_subgroup {R : Type u} [ring R] {s : subring R} {x : R} :
x s
@[simp]
theorem subring.coe_to_add_subgroup {R : Type u} [ring R] (s : subring R) :

## top #

@[protected, instance]
def subring.has_top {R : Type u} [ring R] :

The subring `R` of the ring `R`.

Equations
@[simp]
theorem subring.mem_top {R : Type u} [ring R] (x : R) :
@[simp]
theorem subring.coe_top {R : Type u} [ring R] :

## comap #

def subring.comap {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (s : subring S) :

The preimage of a subring along a ring homomorphism is a subring.

Equations
@[simp]
theorem subring.coe_comap {R : Type u} {S : Type v} [ring R] [ring S] (s : subring S) (f : R →+* S) :
@[simp]
theorem subring.mem_comap {R : Type u} {S : Type v} [ring R] [ring S] {s : subring S} {f : R →+* S} {x : R} :
x f x s
theorem subring.comap_comap {R : Type u} {S : Type v} {T : Type w} [ring R] [ring S] [ring T] (s : subring T) (g : S →+* T) (f : R →+* S) :
s) = subring.comap (g.comp f) s

## map #

def subring.map {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (s : subring R) :

The image of a subring along a ring homomorphism is a subring.

Equations
@[simp]
theorem subring.coe_map {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (s : subring R) :
s) = f '' s
@[simp]
theorem subring.mem_map {R : Type u} {S : Type v} [ring R] [ring S] {f : R →+* S} {s : subring R} {y : S} :
y s ∃ (x : R) (H : x s), f x = y
@[simp]
theorem subring.map_id {R : Type u} [ring R] (s : subring R) :
s = s
theorem subring.map_map {R : Type u} {S : Type v} {T : Type w} [ring R] [ring S] [ring T] (s : subring R) (g : S →+* T) (f : R →+* S) :
s) = subring.map (g.comp f) s
theorem subring.map_le_iff_le_comap {R : Type u} {S : Type v} [ring R] [ring S] {f : R →+* S} {s : subring R} {t : subring S} :
s t s
theorem subring.gc_map_comap {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) :
noncomputable def subring.equiv_map_of_injective {R : Type u} {S : Type v} [ring R] [ring S] (s : subring R) (f : R →+* S) (hf : function.injective f) :

A subring is isomorphic to its image under an injective function

Equations
@[simp]
theorem subring.coe_equiv_map_of_injective_apply {R : Type u} {S : Type v} [ring R] [ring S] (s : subring R) (f : R →+* S) (hf : function.injective f) (x : s) :
( hf) x) = f x

## range #

def ring_hom.range {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) :

The range of a ring homomorphism, as a subring of the target. See Note [range copy pattern].

Equations
Instances for `↥ring_hom.range`
@[simp]
theorem ring_hom.coe_range {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) :
(f.range) =
@[simp]
theorem ring_hom.mem_range {R : Type u} {S : Type v} [ring R] [ring S] {f : R →+* S} {y : S} :
y f.range ∃ (x : R), f x = y
theorem ring_hom.range_eq_map {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) :
f.range =
theorem ring_hom.mem_range_self {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (x : R) :
theorem ring_hom.map_range {R : Type u} {S : Type v} {T : Type w} [ring R] [ring S] [ring T] (g : S →+* T) (f : R →+* S) :
f.range = (g.comp f).range
@[protected, instance]
def ring_hom.fintype_range {R : Type u} {S : Type v} [ring R] [ring S] [fintype R] [decidable_eq S] (f : R →+* S) :

The range of a ring homomorphism is a fintype, if the domain is a fintype. Note: this instance can form a diamond with `subtype.fintype` in the presence of `fintype S`.

Equations

## bot #

@[protected, instance]
def subring.has_bot {R : Type u} [ring R] :
Equations
@[protected, instance]
def subring.inhabited {R : Type u} [ring R] :
Equations
theorem subring.coe_bot {R : Type u} [ring R] :
theorem subring.mem_bot {R : Type u} [ring R] {x : R} :
x ∃ (n : ), n = x

## inf #

@[protected, instance]
def subring.has_inf {R : Type u} [ring R] :

The inf of two subrings is their intersection.

Equations
@[simp]
theorem subring.coe_inf {R : Type u} [ring R] (p p' : subring R) :
(p p') = p p'
@[simp]
theorem subring.mem_inf {R : Type u} [ring R] {p p' : subring R} {x : R} :
x p p' x p x p'
@[protected, instance]
def subring.has_Inf {R : Type u} [ring R] :
Equations
@[simp, norm_cast]
theorem subring.coe_Inf {R : Type u} [ring R] (S : set (subring R)) :
(has_Inf.Inf S) = ⋂ (s : subring R) (H : s S), s
theorem subring.mem_Inf {R : Type u} [ring R] {S : set (subring R)} {x : R} :
x ∀ (p : subring R), p Sx p
@[simp]
theorem subring.Inf_to_submonoid {R : Type u} [ring R] (s : set (subring R)) :
= ⨅ (t : subring R) (H : t s), t.to_submonoid
@[simp]
theorem subring.Inf_to_add_subgroup {R : Type u} [ring R] (s : set (subring R)) :
= ⨅ (t : subring R) (H : t s), t.to_add_subgroup
@[protected, instance]
def subring.complete_lattice {R : Type u} [ring R] :

Subrings of a ring form a complete lattice.

Equations
theorem subring.eq_top_iff' {R : Type u} [ring R] (A : subring R) :
A = ∀ (x : R), x A

## Center of a ring #

def subring.center (R : Type u) [ring R] :

The center of a ring `R` is the set of elements that commute with everything in `R`

Equations
Instances for `↥subring.center`
theorem subring.coe_center (R : Type u) [ring R] :
@[simp]
theorem subring.center_to_subsemiring (R : Type u) [ring R] :
theorem subring.mem_center_iff {R : Type u} [ring R] {z : R} :
∀ (g : R), g * z = z * g
@[protected, instance]
def subring.decidable_mem_center {R : Type u} [ring R] [decidable_eq R] [fintype R] :
decidable_pred (λ (_x : R), _x subring.center R)
Equations
@[simp]
theorem subring.center_eq_top (R : Type u_1) [comm_ring R] :
@[protected, instance]
def subring.center.comm_ring {R : Type u} [ring R] :

The center is commutative.

Equations
@[protected, instance]
def subring.center.field {K : Type u}  :
Equations
@[simp]
theorem subring.center.coe_inv {K : Type u} (a : ) :
@[simp]
theorem subring.center.coe_div {K : Type u} (a b : ) :
(a / b) = a / b

## subring closure of a subset #

def subring.closure {R : Type u} [ring R] (s : set R) :

The `subring` generated by a set.

Equations
theorem subring.mem_closure {R : Type u} [ring R] {x : R} {s : set R} :
∀ (S : subring R), s Sx S
@[simp]
theorem subring.subset_closure {R : Type u} [ring R] {s : set R} :

The subring generated by a set includes the set.

theorem subring.not_mem_of_not_mem_closure {R : Type u} [ring R] {s : set R} {P : R} (hP : P ) :
P s
@[simp]
theorem subring.closure_le {R : Type u} [ring R] {s : set R} {t : subring R} :
s t

A subring `t` includes `closure s` if and only if it includes `s`.

theorem subring.closure_mono {R : Type u} [ring R] ⦃s t : set R⦄ (h : s t) :

Subring closure of a set is monotone in its argument: if `s ⊆ t`, then `closure s ≤ closure t`.

theorem subring.closure_eq_of_le {R : Type u} [ring R] {s : set R} {t : subring R} (h₁ : s t) (h₂ : t ) :
theorem subring.closure_induction {R : Type u} [ring R] {s : set R} {p : R → Prop} {x : R} (h : x ) (Hs : ∀ (x : R), x sp x) (H0 : p 0) (H1 : p 1) (Hadd : ∀ (x y : R), p xp yp (x + y)) (Hneg : ∀ (x : R), p xp (-x)) (Hmul : ∀ (x y : R), p xp yp (x * y)) :
p x

An induction principle for closure membership. If `p` holds for `0`, `1`, and all elements of `s`, and is preserved under addition, negation, and multiplication, then `p` holds for all elements of the closure of `s`.

theorem subring.closure_induction₂ {R : Type u} [ring R] {s : set R} {p : R → R → Prop} {a b : R} (ha : a ) (hb : b ) (Hs : ∀ (x : R), x s∀ (y : R), y sp x y) (H0_left : ∀ (x : R), p 0 x) (H0_right : ∀ (x : R), p x 0) (H1_left : ∀ (x : R), p 1 x) (H1_right : ∀ (x : R), p x 1) (Hneg_left : ∀ (x y : R), p x yp (-x) y) (Hneg_right : ∀ (x y : R), p x yp x (-y)) (Hadd_left : ∀ (x₁ x₂ y : R), p x₁ yp x₂ yp (x₁ + x₂) y) (Hadd_right : ∀ (x y₁ y₂ : R), p x y₁p x y₂p x (y₁ + y₂)) (Hmul_left : ∀ (x₁ x₂ y : R), p x₁ yp x₂ yp (x₁ * x₂) y) (Hmul_right : ∀ (x y₁ y₂ : R), p x y₁p x y₂p x (y₁ * y₂)) :
p a b

An induction principle for closure membership, for predicates with two arguments.

theorem subring.mem_closure_iff {R : Type u} [ring R] {s : set R} {x : R} :
def subring.closure_comm_ring_of_comm {R : Type u} [ring R] {s : set R} (hcomm : ∀ (a : R), a s∀ (b : R), b sa * b = b * a) :

If all elements of `s : set A` commute pairwise, then `closure s` is a commutative ring.

Equations
theorem subring.exists_list_of_mem_closure {R : Type u} [ring R] {s : set R} {x : R} (h : x ) :
∃ (L : list (list R)), (∀ (t : list R), t L∀ (y : R), y ty s y = -1) .sum = x
@[protected]
def subring.gi (R : Type u) [ring R] :

`closure` forms a Galois insertion with the coercion to set.

Equations
theorem subring.closure_eq {R : Type u} [ring R] (s : subring R) :

Closure of a subring `S` equals `S`.

@[simp]
theorem subring.closure_empty {R : Type u} [ring R] :
@[simp]
theorem subring.closure_univ {R : Type u} [ring R] :
theorem subring.closure_union {R : Type u} [ring R] (s t : set R) :
theorem subring.closure_Union {R : Type u} [ring R] {ι : Sort u_1} (s : ι → set R) :
subring.closure (⋃ (i : ι), s i) = ⨆ (i : ι), subring.closure (s i)
theorem subring.closure_sUnion {R : Type u} [ring R] (s : set (set R)) :
= ⨆ (t : set R) (H : t s),
theorem subring.map_sup {R : Type u} {S : Type v} [ring R] [ring S] (s t : subring R) (f : R →+* S) :
(s t) = s t
theorem subring.map_supr {R : Type u} {S : Type v} [ring R] [ring S] {ι : Sort u_1} (f : R →+* S) (s : ι → ) :
(supr s) = ⨆ (i : ι), (s i)
theorem subring.comap_inf {R : Type u} {S : Type v} [ring R] [ring S] (s t : subring S) (f : R →+* S) :
(s t) =
theorem subring.comap_infi {R : Type u} {S : Type v} [ring R] [ring S] {ι : Sort u_1} (f : R →+* S) (s : ι → ) :
(infi s) = ⨅ (i : ι), (s i)
@[simp]
theorem subring.map_bot {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) :
@[simp]
theorem subring.comap_top {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) :
def subring.prod {R : Type u} {S : Type v} [ring R] [ring S] (s : subring R) (t : subring S) :
subring (R × S)

Given `subring`s `s`, `t` of rings `R`, `S` respectively, `s.prod t` is `s ×̂ t` as a subring of `R × S`.

Equations
@[norm_cast]
theorem subring.coe_prod {R : Type u} {S : Type v} [ring R] [ring S] (s : subring R) (t : subring S) :
(s.prod t) = s ×ˢ t
theorem subring.mem_prod {R : Type u} {S : Type v} [ring R] [ring S] {s : subring R} {t : subring S} {p : R × S} :
p s.prod t p.fst s p.snd t
theorem subring.prod_mono {R : Type u} {S : Type v} [ring R] [ring S] ⦃s₁ s₂ : subring R⦄ (hs : s₁ s₂) ⦃t₁ t₂ : subring S⦄ (ht : t₁ t₂) :
s₁.prod t₁ s₂.prod t₂
theorem subring.prod_mono_right {R : Type u} {S : Type v} [ring R] [ring S] (s : subring R) :
monotone (λ (t : subring S), s.prod t)
theorem subring.prod_mono_left {R : Type u} {S : Type v} [ring R] [ring S] (t : subring S) :
monotone (λ (s : subring R), s.prod t)
theorem subring.prod_top {R : Type u} {S : Type v} [ring R] [ring S] (s : subring R) :
s.prod = s
theorem subring.top_prod {R : Type u} {S : Type v} [ring R] [ring S] (s : subring S) :
.prod s = s
@[simp]
theorem subring.top_prod_top {R : Type u} {S : Type v} [ring R] [ring S] :
def subring.prod_equiv {R : Type u} {S : Type v} [ring R] [ring S] (s : subring R) (t : subring S) :

Product of subrings is isomorphic to their product as rings.

Equations
theorem subring.mem_supr_of_directed {R : Type u} [ring R] {ι : Sort u_1} [hι : nonempty ι] {S : ι → } (hS : S) {x : R} :
(x ⨆ (i : ι), S i) ∃ (i : ι), x S i

The underlying set of a non-empty directed Sup of subrings is just a union of the subrings. Note that this fails without the directedness assumption (the union of two subrings is typically not a subring)

theorem subring.coe_supr_of_directed {R : Type u} [ring R] {ι : Sort u_1} [hι : nonempty ι] {S : ι → } (hS : S) :
(⨆ (i : ι), S i) = ⋃ (i : ι), (S i)
theorem subring.mem_Sup_of_directed_on {R : Type u} [ring R] {S : set (subring R)} (Sne : S.nonempty) (hS : S) {x : R} :
x ∃ (s : subring R) (H : s S), x s
theorem subring.coe_Sup_of_directed_on {R : Type u} [ring R] {S : set (subring R)} (Sne : S.nonempty) (hS : S) :
(has_Sup.Sup S) = ⋃ (s : subring R) (H : s S), s
theorem subring.mem_map_equiv {R : Type u} {S : Type v} [ring R] [ring S] {f : R ≃+* S} {K : subring R} {x : S} :
x K (f.symm) x K
theorem subring.map_equiv_eq_comap_symm {R : Type u} {S : Type v} [ring R] [ring S] (f : R ≃+* S) (K : subring R) :
K = K
theorem subring.comap_equiv_eq_map_symm {R : Type u} {S : Type v} [ring R] [ring S] (f : R ≃+* S) (K : subring S) :
def ring_hom.range_restrict {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) :

Restriction of a ring homomorphism to its range interpreted as a subsemiring.

This is the bundled version of `set.range_factorization`.

Equations
@[simp]
theorem ring_hom.coe_range_restrict {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (x : R) :
theorem ring_hom.range_restrict_surjective {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) :
theorem ring_hom.range_top_iff_surjective {R : Type u} {S : Type v} [ring R] [ring S] {f : R →+* S} :
theorem ring_hom.range_top_of_surjective {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (hf : function.surjective f) :

The range of a surjective ring homomorphism is the whole of the codomain.

def ring_hom.eq_locus {R : Type u} {S : Type v} [ring R] [ring S] (f g : R →+* S) :

The subring of elements `x : R` such that `f x = g x`, i.e., the equalizer of f and g as a subring of R

Equations
theorem ring_hom.eq_on_set_closure {R : Type u} {S : Type v} [ring R] [ring S] {f g : R →+* S} {s : set R} (h : g s) :

If two ring homomorphisms are equal on a set, then they are equal on its subring closure.

theorem ring_hom.eq_of_eq_on_set_top {R : Type u} {S : Type v} [ring R] [ring S] {f g : R →+* S} (h : g ) :
f = g
theorem ring_hom.eq_of_eq_on_set_dense {R : Type u} {S : Type v} [ring R] [ring S] {s : set R} (hs : = ) {f g : R →+* S} (h : g s) :
f = g
theorem ring_hom.closure_preimage_le {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (s : set S) :
theorem ring_hom.map_closure {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (s : set R) :

The image under a ring homomorphism of the subring generated by a set equals the subring generated by the image of the set.

def subring.inclusion {R : Type u} [ring R] {S T : subring R} (h : S T) :

The ring homomorphism associated to an inclusion of subrings.

Equations
@[simp]
theorem subring.range_subtype {R : Type u} [ring R] (s : subring R) :
@[simp]
theorem subring.range_fst {R : Type u} {S : Type v} [ring R] [ring S] :
@[simp]
theorem subring.range_snd {R : Type u} {S : Type v} [ring R] [ring S] :
@[simp]
theorem subring.prod_bot_sup_bot_prod {R : Type u} {S : Type v} [ring R] [ring S] (s : subring R) (t : subring S) :
def ring_equiv.subring_congr {R : Type u} [ring R] {s t : subring R} (h : s = t) :

Makes the identity isomorphism from a proof two subrings of a multiplicative monoid are equal.

Equations
def ring_equiv.of_left_inverse {R : Type u} {S : Type v} [ring R] [ring S] {g : S → R} {f : R →+* S} (h : f) :

Restrict a ring homomorphism with a left inverse to a ring isomorphism to its `ring_hom.range`.

Equations
@[simp]
theorem ring_equiv.of_left_inverse_apply {R : Type u} {S : Type v} [ring R] [ring S] {g : S → R} {f : R →+* S} (h : f) (x : R) :
x) = f x
@[simp]
theorem ring_equiv.of_left_inverse_symm_apply {R : Type u} {S : Type v} [ring R] [ring S] {g : S → R} {f : R →+* S} (h : f) (x : (f.range)) :
x = g x
@[simp]
theorem ring_equiv.subring_map_symm_apply_coe {R : Type u} {S : Type v} [ring R] [ring S] {s : subring R} (e : R ≃+* S)  :
@[simp]
theorem ring_equiv.subring_map_apply_coe {R : Type u} {S : Type v} [ring R] [ring S] {s : subring R} (e : R ≃+* S) (ᾰ : (s.to_subsemiring.to_add_submonoid)) :
((e.subring_map) ᾰ) = e
def ring_equiv.subring_map {R : Type u} {S : Type v} [ring R] [ring S] {s : subring R} (e : R ≃+* S) :

Given an equivalence `e : R ≃+* S` of rings and a subring `s` of `R`, `subring_equiv_map e s` is the induced equivalence between `s` and `s.map e`

Equations
@[protected]
theorem subring.in_closure.rec_on {R : Type u} [ring R] {s : set R} {C : R → Prop} {x : R} (hx : x ) (h1 : C 1) (hneg1 : C (-1)) (hs : ∀ (z : R), z s∀ (n : R), C nC (z * n)) (ha : ∀ {x y : R}, C xC yC (x + y)) :
C x
theorem subring.closure_preimage_le {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (s : set S) :
theorem add_subgroup.int_mul_mem {R : Type u} [ring R] {G : add_subgroup R} (k : ) {g : R} (h : g G) :
k * g G

## Actions by `subring`s #

These are just copies of the definitions about `subsemiring` starting from `subsemiring.mul_action`.

When `R` is commutative, `algebra.of_subring` provides a stronger result than those found in this file, which uses the same scalar action.

@[protected, instance]
def subring.has_scalar {R : Type u} [ring R] {α : Type u_1} [ α] (S : subring R) :
α

The action by a subring is the action by the underlying ring.

Equations
theorem subring.smul_def {R : Type u} [ring R] {α : Type u_1} [ α] {S : subring R} (g : S) (m : α) :
g m = g m
@[protected, instance]
def subring.smul_comm_class_left {R : Type u} [ring R] {α : Type u_1} {β : Type u_2} [ β] [ β] [ β] (S : subring R) :
β
@[protected, instance]
def subring.smul_comm_class_right {R : Type u} [ring R] {α : Type u_1} {β : Type u_2} [ β] [ β] [ β] (S : subring R) :
β
@[protected, instance]
def subring.is_scalar_tower {R : Type u} [ring R] {α : Type u_1} {β : Type u_2} [ β] [ α] [ β] [ β] (S : subring R) :
β

Note that this provides `is_scalar_tower S R R` which is needed by `smul_mul_assoc`.

@[protected, instance]
def subring.has_faithful_smul {R : Type u} [ring R] {α : Type u_1} [ α] [ α] (S : subring R) :
@[protected, instance]
def subring.mul_action {R : Type u} [ring R] {α : Type u_1} [ α] (S : subring R) :
α

The action by a subring is the action by the underlying ring.

Equations
@[protected, instance]
def subring.distrib_mul_action {R : Type u} [ring R] {α : Type u_1} [add_monoid α] [ α] (S : subring R) :

The action by a subring is the action by the underlying ring.

Equations
@[protected, instance]
def subring.mul_distrib_mul_action {R : Type u} [ring R] {α : Type u_1} [monoid α] (S : subring R) :

The action by a subring is the action by the underlying ring.

Equations
@[protected, instance]
def subring.smul_with_zero {R : Type u} [ring R] {α : Type u_1} [has_zero α] [ α] (S : subring R) :

The action by a subring is the action by the underlying ring.

Equations
@[protected, instance]
def subring.mul_action_with_zero {R : Type u} [ring R] {α : Type u_1} [has_zero α] [ α] (S : subring R) :

The action by a subring is the action by the underlying ring.

Equations
@[protected, instance]
def subring.module {R : Type u} [ring R] {α : Type u_1} [ α] (S : subring R) :
α

The action by a subring is the action by the underlying ring.

Equations
@[protected, instance]
def subring.center.smul_comm_class_left {R : Type u} [ring R] :
R

The center of a semiring acts commutatively on that semiring.

@[protected, instance]
def subring.center.smul_comm_class_right {R : Type u} [ring R] :
R

The center of a semiring acts commutatively on that semiring.

def units.pos_subgroup (R : Type u_1)  :

The subgroup of positive units of a linear ordered semiring.

Equations
@[simp]
theorem units.mem_pos_subgroup {R : Type u_1} (u : Rˣ) :
0 < u