# mathlibdocumentation

ring_theory.subring

# 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.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

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.

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
@[simp]
theorem subring.mem_carrier {R : Type u} [ring R] {s : subring R} {x : R} :
x s.carrier x 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
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 set.to_subring {R : Type u} [ring R] (S : set R) [is_subring S] :

Construct a subring from a set satisfying is_subring.

Equations
def subsemiring.to_subring {R : Type u} [ring R] (s : subsemiring R) (hneg : -1 s) :

A subsemiring containing -1 is a subring.

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

A subring contains the ring's 1.

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

A subring contains the ring's 0.

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.

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.

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

A subring is closed under negation.

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

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.

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.

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.

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.

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) :
∏ (i : ι) in t, f i s

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

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) :
∑ (i : ι) in t, f i s

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

theorem subring.pow_mem {R : Type u} [ring R] (s : subring R) {x : R} (hx : x s) (n : ) :
x ^ n s
theorem subring.gsmul_mem {R : Type u} [ring R] (s : subring R) {x : R} (hx : x s) (n : ) :
n x s
theorem subring.coe_int_mem {R : Type u} [ring R] (s : subring R) (n : ) :
n s
@[protected, instance]
def subring.to_ring {R : Type u} [ring R] (s : subring R) :

A subring of a ring inherits a ring structure

Equations
@[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.integral_domain {R : Type u_1} (s : subring R) :

A subring of an integral domain is an integral domain.

Equations
@[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
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) :

# 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
@[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
def ring_hom.cod_restrict' {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (s : subring S) (h : ∀ (x : R), f x s) :

Restrict the codomain of a ring homomorphism to a subring that includes the range.

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)) :
(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 Inf S ∀ (p : subring R), p Sx p
@[simp]
theorem subring.Inf_to_submonoid {R : Type u} [ring R] (s : set (subring R)) :
(Inf s).to_submonoid = ⨅ (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)) :
(Inf s).to_add_subgroup = ⨅ (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

# 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.

@[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.mem_closure_iff {R : Type u} [ring R] {s : set R} {x : R} :
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 subrings 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.prod 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 Sup S ∃ (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) :
(Sup S) = ⋃ (s : subring R) (H : s S), s
def ring_hom.restrict {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (s : subring R) :

Restriction of a ring homomorphism to a subring of the domain.

Equations
@[simp]
theorem ring_hom.restrict_apply {R : Type u} {S : Type v} [ring R] [ring S] {s : subring R} (f : R →+* S) (x : s) :
(f.restrict s) x = f x
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
@[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