mathlib documentation

deprecated.subring

@[class]
structure is_subring {R : Type u} [ring R] :
set R → Prop

S is a subring: a set containing 1 and closed under multiplication, addition and and additive inverse.

Instances
def subtype.ring {R : Type u} [ring R] {S : set R} [is_subring S] :

The ring structure on a subring coerced to a type.

Equations
@[instance]
def ring_hom.is_subring_preimage {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (s : set S) [is_subring s] :

@[instance]
def ring_hom.is_subring_image {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (s : set R) [is_subring s] :

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

def ring_hom.cod_restrict {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) (s : set S) [is_subring s] :
(∀ (x : R), f x s)R →+* s

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

Equations
def is_subring.subtype {R : Type u} [ring R] (S : set R) [is_subring S] :

Coersion S → R as a ring homormorphism

Equations
@[simp]
theorem is_subring.coe_subtype {R : Type u} [ring R] {S : set R} [is_subring S] :

def subset.comm_ring {cR : Type u} [comm_ring cR] {S : set cR} [is_subring S] :

The commutative ring structure on a subring coerced to a type.

Equations
def subtype.comm_ring {cR : Type u} [comm_ring cR] {S : set cR} [is_subring S] :

The commutative ring structure on a subring coerced to a type.

Equations
def subring.domain {D : Type u_1} [integral_domain D] (S : set D) [is_subring S] :

The integral domain structure on a subring of an integral domain coerced to a type.

Equations
@[instance]
def is_subring.inter {R : Type u} [ring R] (S₁ S₂ : set R) [is_subring S₁] [is_subring S₂] :
is_subring (S₁ S₂)

@[instance]
def is_subring.Inter {R : Type u} [ring R] {ι : Sort u_1} (S : ι → set R) [h : ∀ (y : ι), is_subring (S y)] :

theorem is_subring_Union_of_directed {R : Type u} [ring R] {ι : Type u_1} [hι : nonempty ι] (s : ι → set R) [∀ (i : ι), is_subring (s i)] :
(∀ (i j : ι), ∃ (k : ι), s i s k s j s k)is_subring (⋃ (i : ι), s i)

def ring.closure {R : Type u} [ring R] :
set Rset R

Equations
theorem ring.exists_list_of_mem_closure {R : Type u} [ring R] {s : set R} {a : R} :
a ring.closure s(∃ (L : list (list R)), (∀ (l : list R), l L∀ (x : R), x lx s x = -1) (list.map list.prod L).sum = a)

theorem ring.in_closure.rec_on {R : Type u} [ring R] {s : set R} {C : R → Prop} {x : R} :
x ring.closure sC 1C (-1)(∀ (z : R), z s∀ (n : R), C nC (z * n))(∀ {x y : R}, C xC yC (x + y))C x

@[instance]
def ring.is_subring {R : Type u} [ring R] {s : set R} :

theorem ring.mem_closure {R : Type u} [ring R] {s : set R} {a : R} :
a sa ring.closure s

theorem ring.subset_closure {R : Type u} [ring R] {s : set R} :

theorem ring.closure_subset {R : Type u} [ring R] {s t : set R} [is_subring t] :
s tring.closure s t

theorem ring.closure_subset_iff {R : Type u} [ring R] (s t : set R) [is_subring t] :

theorem ring.closure_mono {R : Type u} [ring R] {s t : set R} :

theorem ring.image_closure {R : Type u} [ring R] {S : Type u_1} [ring S] (f : R →+* S) (s : set R) :