Documentation

Mathlib.Deprecated.Subring

Unbundled subrings (deprecated) #

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 RingTheory.Subring.Basic, for subrings of rings.

Main definitions #

IsSubring (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 #

IsSubring

source
structure IsSubring {R : Type u} [Ring R] (S : Set R) extends IsAddSubgroup , IsSubmonoid :
Prop

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

    Instances For
      source
      def IsSubring.subring {R : Type u} [Ring R] {S : Set R} (hs : IsSubring S) :
      Subring R

      Construct a Subring from a set satisfying IsSubring.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem RingHom.isSubring_preimage {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) {s : Set S} (hs : IsSubring s) :
        IsSubring (⇑f ⁻¹' s)
        source
        theorem RingHom.isSubring_image {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) {s : Set R} (hs : IsSubring s) :
        IsSubring (⇑f '' s)
        source
        theorem RingHom.isSubring_set_range {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) :
        IsSubring (Set.range ⇑f)
        source
        theorem IsSubring.inter {R : Type u} [Ring R] {S₁ : Set R} {S₂ : Set R} (hS₁ : IsSubring S₁) (hS₂ : IsSubring S₂) :
        IsSubring (S₁ ∩ S₂)
        source
        theorem IsSubring.iInter {R : Type u} [Ring R] {ι : Sort u_1} {S : ι → Set R} (h : ∀ (y : ι), IsSubring (S y)) :
        IsSubring (Set.iInter S)
        source
        theorem isSubring_iUnion_of_directed {R : Type u} [Ring R] {ι : Type u_1} [Nonempty ι] {s : ι → Set R} (h : ∀ (i : ι), IsSubring (s i)) (directed : ∀ (i j : ι), ∃ (k : ι), s i ⊆ s k ∧ s j ⊆ s k) :
        IsSubring (⋃ (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
        Instances For
          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 ∈ L, ∀ x ∈ l, x ∈ s ∨ x = -1) ∧ List.sum (List.map List.prod L) = a
          source
          theorem Ring.InClosure.recOn {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 ∈ 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.isSubring {R : Type u} [Ring R] {s : Set R} :
          IsSubring (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 : Set R} {t : Set R} (ht : IsSubring t) :
          s ⊆ t → Ring.closure s ⊆ t
          source
          theorem Ring.closure_subset_iff {R : Type u} [Ring R] {s : Set R} {t : Set R} (ht : IsSubring t) :
          Ring.closure s ⊆ t ↔ s ⊆ t
          source
          theorem Ring.closure_mono {R : Type u} [Ring R] {s : Set R} {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)