mathlib docs: deprecated.subring

source

@[class]

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

Prop

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 and additive inverse.

Instances

source

@[instance]

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

ring ↥S

Equations

subset.ring = {add := add_comm_group.add subtype.add_comm_group, add_assoc := _, zero := add_comm_group.zero subtype.add_comm_group, zero_add := _, add_zero := _, neg := add_comm_group.neg subtype.add_comm_group, add_left_neg := _, add_comm := _, mul := monoid.mul subtype.monoid, mul_assoc := _, one := monoid.one subtype.monoid, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _}

source

@[instance]

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

ring (subtype S)

Equations

subtype.ring = subset.ring

source

@[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] :

is_subring (⇑f ⁻¹' s)

source

@[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] :

is_subring (⇑f '' s)

source

@[instance]

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

is_subring (set.range ⇑f)

source

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

R →+* ↥s

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

Equations

f.cod_restrict s h = {to_fun := λ (x : R), ⟨⇑f x, _⟩, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

source

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

↥S →+* R

Coersion S → R as a ring homormorphism

Equations

is_subring.subtype S = {to_fun := coe coe_to_lift, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

source

@[simp]

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

⇑(is_subring.subtype S) = coe

source

@[instance]

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

comm_ring ↥S

Equations

subset.comm_ring = {add := ring.add subset.ring, add_assoc := _, zero := ring.zero subset.ring, zero_add := _, add_zero := _, neg := ring.neg subset.ring, add_left_neg := _, add_comm := _, mul := ring.mul subset.ring, mul_assoc := _, one := ring.one subset.ring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _}

source

@[instance]

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

comm_ring (subtype S)

Equations

subtype.comm_ring = subset.comm_ring

source

@[instance]

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

integral_domain ↥S

Equations

subring.domain S = {add := comm_ring.add subset.comm_ring, add_assoc := _, zero := comm_ring.zero subset.comm_ring, zero_add := _, add_zero := _, neg := comm_ring.neg subset.comm_ring, add_left_neg := _, add_comm := _, mul := comm_ring.mul subset.comm_ring, mul_assoc := _, one := comm_ring.one subset.comm_ring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}

source

@[instance]

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

is_subring (S₁ ∩ S₂)

source

@[instance]

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

is_subring (set.Inter S)

source

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

is_subring (⋃ (i : ι), s i)

source

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

set R

Equations

ring.closure s = add_group.closure (monoid.closure s)

source

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 ∈ l → x ∈ s ∨ x = -1) ∧ (list.map list.prod L).sum = a

source

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 n → C (z * n)) (ha : ∀ {x y : R}, C x → C y → C (x + y)) :

C x

source

@[instance]

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

is_subring (ring.closure s)

source

theorem ring.mem_closure {R : Type u} [ring R] {s : set R} {a : R} (a_1 : a ∈ s) :

a ∈ ring.closure s

source

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

s ⊆ ring.closure s

source

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

ring.closure s ⊆ t

source

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

ring.closure s ⊆ t ↔ s ⊆ t

source

theorem ring.closure_mono {R : Type u} [ring R] {s t : set R} (H : s ⊆ t) :

ring.closure s ⊆ ring.closure t

source

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

⇑f '' ring.closure s = ring.closure (⇑f '' s)