mathlib documentation

deprecated.subring

structure is_subring {R : Type u} [ring R] (S : set R) :
Prop

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

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

Construct a subring from a set satisfying is_subring.

Equations
theorem ring_hom.is_subring_preimage {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) {s : set S} (hs : is_subring s) :
theorem ring_hom.is_subring_image {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) {s : set R} (hs : is_subring s) :
theorem ring_hom.is_subring_set_range {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S) :
theorem is_subring.inter {R : Type u} [ring R] {S₁ S₂ : set R} (hS₁ : is_subring S₁) (hS₂ : is_subring S₂) :
is_subring (S₁ S₂)
theorem 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} (h : ∀ (i : ι), is_subring (s i)) (directed : ∀ (i j : ι), ∃ (k : ι), s i s k s j s k) :
is_subring (⋃ (i : ι), s i)
def ring.closure {R : Type u} [ring R] (s : set R) :
set R
Equations
theorem ring.exists_list_of_mem_closure {R : Type u} [ring R] {s : set R} {a : R} (h : 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} (hx : x ring.closure s) (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 ring.closure.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} (ht : is_subring t) :
s tring.closure s t
theorem ring.closure_subset_iff {R : Type u} [ring R] {s t : set R} (ht : is_subring t) :
theorem ring.closure_mono {R : Type u} [ring R] {s t : set R} (H : s t) :
theorem ring.image_closure {R : Type u} [ring R] {S : Type u_1} [ring S] (f : R →+* S) (s : set R) :