mathlib3 documentation

deprecated.subring

Unbundled subrings (deprecated) #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file is deprecated, and is no longer imported by anything in mathlib other than other deprecated files, and test files. You should not need to import it.

This file defines predicates for unbundled subrings. Instead of using this file, please use subring, defined in ring_theory.subring.basic, for subrings of rings.

Main definitions #

is_subring (S : set R) : Prop : the predicate that S is the underlying set of a subring of the ring R. The bundled variant subring R should be used in preference to this.

Tags #

is_subring

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

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

Construct a subring from a set satisfying is_subring.

Equations
source
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) :
is_subring (⇑f ⁻¹' s)
source
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) :
is_subring (⇑f '' s)
source
theorem 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
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₂)
source
theorem 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} (h : ∀ (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

The smallest subring containing a given subset of a ring, considered as a set. This function is deprecated; use subring.closure.

Equations
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
@[protected]
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
theorem ring.closure.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 ∈ 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} (ht : is_subring t) :
s ⊆ t → ring.closure s ⊆ t
source
theorem ring.closure_subset_iff {R : Type u} [ring R] {s t : set R} (ht : 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)