Subring.multiset_prod_mem
theorem Subring.multiset_prod_mem :
∀ {R : Type u_1} [inst : CommRing R] (s : Subring R) (m : Multiset R), (∀ a ∈ m, a ∈ s) → m.prod ∈ s
The theorem `Subring.multiset_prod_mem` states that for any commutative ring `R` and any subring `s` of `R`, if all elements of a multiset `m` belong to the subring `s`, then the product of all elements in the multiset `m` also belongs to the subring `s`.
In other words, if we take a multiset from a subring of a commutative ring where all its elements belong to the subring, the product of the multiset's elements will still be in the subring.
More concisely: If `R` is a commutative ring and `s` is a subring of `R` such that all elements in multiset `m` belong to `s`, then the product of elements in `m` belongs to `s`.
|
Subring.subset_closure
theorem Subring.subset_closure : ∀ {R : Type u} [inst : Ring R] {s : Set R}, s ⊆ ↑(Subring.closure s)
The theorem `Subring.subset_closure` states that for any type `R` that forms a Ring, and for any set `s` of elements of the type `R`, the set `s` is a subset of the subring generated by `s` itself. In other words, all the elements of `s` are contained within the subring produced by the `Subring.closure` operation on `s`.
More concisely: For any ring `R` and subset `s` of `R`, `s` is included in the subring generated by `s` (i.e., `Subring.closure s`).
|
Subring.multiset_sum_mem
theorem Subring.multiset_sum_mem :
∀ {R : Type u_1} [inst : Ring R] (s : Subring R) (m : Multiset R), (∀ a ∈ m, a ∈ s) → m.sum ∈ s
This theorem states that for any given ring `R` and a subring `s` of `R`, if we have a multiset `m` of elements from `R` where all elements are in subring `s`, then the sum of all elements in the multiset `m` is also an element of the subring `s`. In other words, the sum of a collection of elements from a subring (with repetitions allowed) is still in that subring.
More concisely: For any ring `R` and subring `s` of `R`, the sum of a multiset of elements from `s` belongs to `s`.
|
Subring.gc_map_comap
theorem Subring.gc_map_comap :
∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S),
GaloisConnection (Subring.map f) (Subring.comap f)
This theorem, `Subring.gc_map_comap`, states that for any two types `R` and `S` with instances of the `Ring` typeclass, and a ring homomorphism `f` from `R` to `S`, there is a Galois connection between the mapping of a subring along `f` and the preimage of a subring along `f`. A Galois connection is a pair of functions that satisfy a certain property: in this case, the mapping of a subring along `f` is less than or equal to a subring in `S` if and only if the original subring in `R` is less than or equal to the preimage of the subring along `f`. This reflects a fundamental duality principle in order theory.
More concisely: Given rings `R` and `S` with ring homomorphism `f` between them, the mapping of a subring of `R` along `f` is equal to the preimage along `f` of the subring of `S` if and only if the original subring of `R` is contained in the preimage along `f`.
|
Subring.sub_mem
theorem Subring.sub_mem : ∀ {R : Type u} [inst : Ring R] (s : Subring R) {x y : R}, x ∈ s → y ∈ s → x - y ∈ s := by
sorry
This theorem states that a subring of a ring is closed under subtraction. In more detail, given any ring `R`, and any `Subring` `s` of `R`, if `x` and `y` are any two elements of `s`, then the result of subtracting `y` from `x` (i.e., `x - y`) is also an element of `s`.
More concisely: If `s` is a subring of a ring `R`, then for all `x, y ∈ s`, `x - y ∈ s`.
|
RingHom.range_top_of_surjective
theorem RingHom.range_top_of_surjective :
∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S), Function.Surjective ⇑f → f.range = ⊤
This theorem states that for any given types `R` and `S` which are rings, if we have a ring homomorphism `f` from `R` to `S` which is surjective, meaning that for every element of `S` there is a corresponding element in `R` such that applying `f` to this element gives the element of `S`, then the range of `f` is equal to the whole of `S` (represented as top `⊤`). In other words, a surjective ring homomorphism maps to every element in the codomain.
More concisely: A surjective ring homomorphism from type `R` to type `S` maps the entire ring `S` to its image, i.e., the range of the homomorphism equals `S`.
|
Subring.closure_induction
theorem Subring.closure_induction :
∀ {R : Type u} [inst : Ring R] {s : Set R} {p : R → Prop} {x : R},
x ∈ Subring.closure s →
(∀ x ∈ s, p x) →
p 0 →
p 1 →
(∀ (x y : R), p x → p y → p (x + y)) →
(∀ (x : R), p x → p (-x)) → (∀ (x y : R), p x → p y → p (x * y)) → p x
This theorem, named `Subring.closure_induction`, is an induction principle for membership in the closure of a set in a ring structure. It states that for any type `R` equipped with a ring structure, any set `s` of elements of `R`, any property `p` applicable to elements of `R`, and any element `x` of `R`, if `x` belongs to the subring generated by `s`, then if `p` holds for all elements of `s`, for `0` and `1`, and is preserved under the operations of addition, negation, and multiplication, then `p` must also hold for `x`. In essence, this theorem allows us to extend properties from a generating set and basic ring elements to the entire generated subring under certain conditions.
More concisely: If `s` is a set of elements in a ring `R`, `p` is a property that holds for all elements in `s`, `0`, and `1`, and is preserved under ring operations, then `p` holds for every element in the subring generated by `s` that contains `x`.
|
Subring.neg_mem
theorem Subring.neg_mem : ∀ {R : Type u} [inst : Ring R] (s : Subring R) {x : R}, x ∈ s → -x ∈ s
This theorem states that for any given Ring `R` and a subring `s` of `R`, if an element `x` is in `s`, then its negation `-x` is also in `s`. In other words, the negation of any element in the subring is also a member of the subring. This property reflects the essence of a subring in ring theory, which is that it is closed under the ring operations, including negation.
More concisely: If `s` is a subring of a ring `R`, then for all `x` in `s`, `-x` is also in `s`.
|
Subring.sum_mem
theorem Subring.sum_mem :
∀ {R : Type u_1} [inst : Ring R] (s : Subring R) {ι : Type u_2} {t : Finset ι} {f : ι → R},
(∀ c ∈ t, f c ∈ s) → (t.sum fun i => f i) ∈ s
The theorem `Subring.sum_mem` states that for any given type `R` which forms a ring, a subring `s` of `R`, a finite set (or `Finset`) `t` indexed by a type `ι`, and a function `f` mapping each element of `Finset` to the ring `R`, if every element `c` in the `Finset` maps to an element in the subring `s` through the function `f`, then the sum of the function values over all elements in the `Finset` also belongs to the subring `s`. In other words, the sum of elements in a subring of a ring, indexed by a finite set, is also in the subring.
More concisely: If `R` is a ring, `s` is a subring of `R`, `t` is a finite set with type `ι`, and `f : ι → R` satisfies `∀ i, f i ∈ s`, then `∑ i in t, f i ∈ s`.
|
Subring.mul_mem
theorem Subring.mul_mem : ∀ {R : Type u} [inst : Ring R] (s : Subring R) {x y : R}, x ∈ s → y ∈ s → x * y ∈ s := by
sorry
This theorem states that a subring is closed under multiplication. In other words, for any ring `R`, and any subring `s` of `R`, if `x` and `y` are any elements of `s`, then the product `x * y` is also an element of `s`. This property is one of the defining characteristics of a subring in ring theory, a branch of abstract algebra.
More concisely: For any ring `R` and subring `s` of `R`, the product of any two elements in `s` belongs to `s`.
|
RingHom.mem_range
theorem RingHom.mem_range :
∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Ring S] {f : R →+* S} {y : S}, y ∈ f.range ↔ ∃ x, f x = y
This theorem states that for any given types `R` and `S` which have a ring structure, a ring homomorphism `f` from `R` to `S`, and an element `y` of `S`, `y` belongs to the range of `f` if and only if there exists an element `x` in `R` such that `f(x)` equals `y`. That is, `y` is in the image of `f` precisely when `y` is the image of some element under `f`.
More concisely: For any ring homomorphisms $f : R \rightarrow S$ and $y \in S$, $y$ is in the image of $f$ if and only if there exists $x \in R$ such that $f(x) = y$.
|
Subring.add_mem
theorem Subring.add_mem : ∀ {R : Type u} [inst : Ring R] (s : Subring R) {x y : R}, x ∈ s → y ∈ s → x + y ∈ s := by
sorry
This theorem states that a subring is closed under addition. In more detail, for any given type `R` which has a ring structure, and any subring `s` of `R`, if you have two elements `x` and `y` from `R` that are members of the subring `s`, then their sum `x + y` is also a member of the subring `s`. This is a fundamental property of subrings in the field of algebra.
More concisely: Given a ring `R` and a subring `s` of `R`, if `x` and `y` are in `s`, then `x + y` is also in `s`.
|
Mathlib.RingTheory.Subring.Basic._auxLemma.14
theorem Mathlib.RingTheory.Subring.Basic._auxLemma.14 : ∀ {R : Type u} [inst : Ring R] (x : R), (x ∈ ⊤) = True := by
sorry
This theorem states that for any type `R` that has a `Ring` structure, any element `x` of `R` belongs to the top (i.e., the whole set `R` itself), denoted as `⊤`. In other words, all elements of a given ring are part of the universal subring.
More concisely: For any ring `R`, every element `x` in `R` belongs to the additive monoid generated by `R`, i.e., `{∃ s : Set, ∀ x : R, x ∈ s ∧ ∀ (a b : R), a + b ∈ s}`.
|
Subring.one_mem
theorem Subring.one_mem : ∀ {R : Type u} [inst : Ring R] (s : Subring R), 1 ∈ s
This theorem states that for any ring `R` and any subring `s` of `R`, the multiplicative identity element `1` of the ring is always an element of the subring `s`. In other words, every subring of a ring must contain the unit or '1' of the parent ring. This is an important property in ring theory that defines the structure of subrings within a ring.
More concisely: For any ring `R` and subring `s` of `R`, the multiplicative identity `1` of `R` belongs to `s`.
|
Subring.mem_comap
theorem Subring.mem_comap :
∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Ring S] {s : Subring S} {f : R →+* S} {x : R},
x ∈ Subring.comap f s ↔ f x ∈ s
This theorem states that for any two types `R` and `S` that have a ring structure, a subring `s` of type `S`, a ring homomorphism `f` from `R` to `S`, and an element `x` of type `R`, the element `x` is in the preimage of the subring `s` under the map `f` if and only if the image of `x` under `f` is in the subring `s`. In other words, it establishes a membership equivalence between the element `x` and its image under the ring homomorphism `f` in the context of subrings and their preimages.
More concisely: For any ring homomorphism $f$ from a ring $R$ to a ring $S$, and any subring $s$ of $S$ and element $x$ in $R$, $x \in f^{-1}(s)$ if and only if $f(x) \in s$.
|
Subring.mem_sInf
theorem Subring.mem_sInf : ∀ {R : Type u} [inst : Ring R] {S : Set (Subring R)} {x : R}, x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
This theorem states that for any given type `R` that is a ring, a set `S` of subrings of `R`, and an element `x` from `R`, `x` is an element of the infimum (greatest lower bound) of `S` if and only if `x` is an element of every `p` in `S`. Essentially, it defines membership in the infimum of a set of subrings: an element belongs to the infimum of a set of subrings if it belongs to every subring in that set.
More concisely: For any ring R, a subset S of subrings of R, and an element x in R, x lies in the infimum of S if and only if x belongs to every subring p in S.
|
coe_int_mem
theorem coe_int_mem :
∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : SetLike S R] [hSR : SubringClass S R] (s : S) (n : ℤ),
↑n ∈ s
This theorem states that for any integer `n`, and any subring `s` of a ring `R`, the integer coercion of `n` always belongs to `s`. Here, `R` and `S` are arbitrary types, where `R` has a ring structure and `S` is a subset of `R` with a `SetLike` structure, satisfying the properties of a subring (`SubringClass`). The integer coercion (`↑n`) maps the integer `n` to an element in the ring `R`. The theorem asserts that this mapped element is indeed in the subring `s`.
More concisely: For any integer `n` and subring `s` of a ring `R` (where `R` has a ring structure and `s` is a subring as defined by `SubringClass`), the integer coercion `↑n` maps `n` to an element in `s`.
|
Subring.prod_mem
theorem Subring.prod_mem :
∀ {R : Type u_1} [inst : CommRing R] (s : Subring R) {ι : Type u_2} {t : Finset ι} {f : ι → R},
(∀ c ∈ t, f c ∈ s) → (t.prod fun i => f i) ∈ s
This theorem states that for any commutative ring `R`, subring `s` of `R`, finite set `t` of any type `ι`, and function `f` from `ι` to `R`, if all elements of `t` mapped through `f` are in `s`, then the product of all such elements, determined by applying `f` to each element of `t` and then taking the product, is also in the subring `s`.
More concisely: If `f` maps a finite set `t` into a commutative ring `s` subring of `R`, then the product of images of elements in `t` under `f` is in `s`.
|
RingHom.rangeRestrict_surjective
theorem RingHom.rangeRestrict_surjective :
∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S), Function.Surjective ⇑f.rangeRestrict
The theorem `RingHom.rangeRestrict_surjective` states that for all rings `R` and `S`, and for every ring homomorphism `f` from `R` to `S`, the function obtained by restricting `f` to its range (i.e., the `rangeRestrict` function) is surjective. In terms of Mathematics, a function is said to be surjective if for every element in the codomain, there is at least one element in the domain of the function that maps to it. Hence, this theorem is essentially stating that every element in the range of the restricted ring homomorphism can be obtained by applying this homomorphism to some element in `R`.
More concisely: For any ring homomorphism between rings `R` and `S`, the restriction of the homomorphism to its range is a surjective function.
|
Subring.mk'.proof_2
theorem Subring.mk'.proof_2 : ∀ {R : Type u_1} [inst : Ring R] (s : Set R) (sa : AddSubgroup R), ↑sa = s → s = ↑sa := by
sorry
This theorem, `Subring.mk'.proof_2`, states that for any type `R` that is a Ring, given a set `s` of elements of `R` and an AddSubgroup `sa` of `R`, if the AddSubgroup `sa` coerced to a set is equal to `s`, then `s` is equal to the AddSubgroup `sa` coerced to a set. This theorem is demonstrating that the equality operation on sets of elements in a Ring and additive subgroups of the Ring is symmetric.
More concisely: For any ring `R`, if the additive subgroup `sa` of `R` equals the set `s` of its elements, then `s` and `sa` coerced to sets are equal.
|
Subring.closure_induction₂
theorem Subring.closure_induction₂ :
∀ {R : Type u} [inst : Ring R] {s : Set R} {p : R → R → Prop} {a b : R},
a ∈ Subring.closure s →
b ∈ Subring.closure s →
(∀ x ∈ s, ∀ y ∈ s, p x y) →
(∀ (x : R), p 0 x) →
(∀ (x : R), p x 0) →
(∀ (x : R), p 1 x) →
(∀ (x : R), p x 1) →
(∀ (x y : R), p x y → p (-x) y) →
(∀ (x y : R), p x y → p x (-y)) →
(∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ + x₂) y) →
(∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ + y₂)) →
(∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ * x₂) y) →
(∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ * y₂)) → p a b
This theorem, named `Subring.closure_induction₂`, provides an induction principle for membership in the closure of a set in a ring. It states that for any ring `R`, set `s` within `R`, and a two-argument predicate `p`, if two elements `a` and `b` belong to the closure of `s` and `p` holds for all pairs of elements in `s`, `p` holds for zero and any element, one and any element, negation of any element and any other element, sum of any two elements and any other element, and product of any two elements and any other element, then `p` holds for `a` and `b`. Essentially, it allows you to induct on the operations of a ring (addition, multiplication, and negation) to prove that a property holds for all elements in the closure of a set within that ring.
More concisely: Given a ring `R`, a set `s` in `R`, and a two-argument predicate `p`, if `a`, `b` are in the closure of `s` and `p` holds for all pairs in `s` and `0`, `1`, `-a`, `a + b`, and `a * b`, then `p` holds for `a` and `b`.
|
Subring.list_prod_mem
theorem Subring.list_prod_mem :
∀ {R : Type u} [inst : Ring R] (s : Subring R) {l : List R}, (∀ x ∈ l, x ∈ s) → l.prod ∈ s
This theorem states that for any given type `R` that has a ring structure, and any subring `s` of `R`, if every element `x` of a list `l` of elements of `R` is in the subring `s`, then the product of the elements in the list `l` is also in the subring `s`.
More concisely: If `R` is a ring and `s` is a subring of `R`, then the product of any list of elements in `s` lies in `s`.
|
Subring.closure_mono
theorem Subring.closure_mono :
∀ {R : Type u} [inst : Ring R] ⦃s t : Set R⦄, s ⊆ t → Subring.closure s ≤ Subring.closure t
This theorem states that the operation of taking the subring closure of a set is monotone with respect to set inclusion in a given ring. In other words, if you have two sets `s` and `t` of elements from a ring `R` such that `s` is a subset of `t`, then the subring generated by `s` is a subring of (or equals to) the subring generated by `t`.
More concisely: If `s` is a subset of `t` in a ring `R`, then the subring generated by `s` is contained in the subring generated by `t`.
|
Subring.closure_eq
theorem Subring.closure_eq : ∀ {R : Type u} [inst : Ring R] (s : Subring R), Subring.closure ↑s = s
This theorem states that for any ring `R`, and a subring `s` of this ring, the closure of the subring `s` is indeed the subring `s` itself. In other words, the closure of a subring does not add any new elements to the subring. In mathematical terms, for all subrings `s` of a ring `R`, the subring generated by the set of elements of `s` is equal to `s`.
More concisely: The subring generated by a subring of a ring is equal to the subring itself.
|
Subring.closure_le
theorem Subring.closure_le :
∀ {R : Type u} [inst : Ring R] {s : Set R} {t : Subring R}, Subring.closure s ≤ t ↔ s ⊆ ↑t
The theorem `Subring.closure_le` states that for any type `R` with a ring structure, and any set `s` of `R` and any subring `t` of `R`, the subring generated by the closure of set `s` is a subset of subring `t` if and only if the set `s` itself is a subset of `subring `t`. This means that a subring `t` includes the closure of `s` precisely when it includes `s` itself.
More concisely: The subring generated by the closure of a set in a ring is contained in the given subring if and only if the original set is contained in the subring.
|
RingHom.eqOn_set_closure
theorem RingHom.eqOn_set_closure :
∀ {R : Type u} [inst : Ring R] {S : Type v} [inst_1 : Semiring S] {f g : R →+* S} {s : Set R},
Set.EqOn (⇑f) (⇑g) s → Set.EqOn ⇑f ⇑g ↑(Subring.closure s)
This theorem states that if two ring homomorphisms, represented by functions `f` and `g` from a ring `R` to a semiring `S`, are equal on a set `s` in `R` (i.e., `f(x) = g(x)` for all `x` in `s`), then these two ring homomorphisms are also equal on the subring closure of that set. Here, the subring closure of a set `s` in `R` is the smallest subring of `R` that contains the set `s`. In other words, any behavior that `f` and `g` share on the original set `s` is preserved when extending their domain to the subring closure of `s`.
More concisely: If two ring homomorphisms agree on a set and its subring closure, they are equal everywhere on the subring.
|
Subring.list_sum_mem
theorem Subring.list_sum_mem :
∀ {R : Type u} [inst : Ring R] (s : Subring R) {l : List R}, (∀ x ∈ l, x ∈ s) → l.sum ∈ s
This theorem states that the sum of a list of elements, all of which belong to a subring of a ring, is also an element of that subring. Here, `R` is any type that has a ring structure, `s` is a subring of `R`, and `l` is a list of elements in `R`. If every element `x` in `l` belongs to `s`, then the sum of `l` is also in `s`. This theorem is an application of the closure property of subrings under addition.
More concisely: If `s` is a subring of a ring `R`, and `l` is a list of elements in `R` all belonging to `s`, then the sum of `l` is also an element of `s`.
|
RingHom.map_closure
theorem RingHom.map_closure :
∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S) (s : Set R),
Subring.map f (Subring.closure s) = Subring.closure (⇑f '' s)
This theorem states that for any ring homomorphism `f` from a ring `R` to a ring `S`, and for any set `s` of elements in `R`, the image under the ring homomorphism `f` of the subring generated by the set `s` in `R` is equal to the subring generated in `S` by the image of the set `s` under `f`. Symbolically, this can be written as `f(Subring.closure(s)) = Subring.closure(f(s))`. This illustrates how the structure of a subring is preserved under a ring homomorphism.
More concisely: For any ring homomorphism between rings `R` and `S`, and any set `s` of elements in `R`, the image under `f` of the subring generated by `s` in `R` equals the subring generated by `f(s)` in `S`.
|
Subring.ext
theorem Subring.ext : ∀ {R : Type u} [inst : Ring R] {S T : Subring R}, (∀ (x : R), x ∈ S ↔ x ∈ T) → S = T
This theorem states that for any type `R` equipped with a ring structure, if `S` and `T` are two subrings of `R` and every element `x` of `R` belongs to `S` if and only if it belongs to `T`, then `S` and `T` are equal. In other words, two subrings of a given ring are considered identical if they contain exactly the same elements.
More concisely: If two subrings of a ring contain the same elements, then they are equal.
|
Subring.mem_iSup_of_directed
theorem Subring.mem_iSup_of_directed :
∀ {R : Type u} [inst : Ring R] {ι : Sort u_1} [hι : Nonempty ι] {S : ι → Subring R},
Directed (fun x x_1 => x ≤ x_1) S → ∀ {x : R}, x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i
This theorem states that for any Ring `R`, let `S` be a directed (according to the 'less than or equal to' relation) family of subrings indexed by some type `ι`, which is nonempty. Then, for any element `x` of `R`, `x` is in the supremum (directed supremum) of the subrings `S i` if and only if there exists some index `i` where `x` is in the subring `S i`. This theorem highlights the fact that the union of all subrings in a directed set of subrings forms a larger subring, but this doesn't hold true if the set is not directed (the union of two arbitrary subrings is typically not a subring itself).
More concisely: For any ring `R` and directed family `S` of subrings of `R` indexed by `ι`, an element `x` of `R` belongs to the supremum of `S` if and only if it belongs to some subring in `S`.
|
Subring.neg_mem'
theorem Subring.neg_mem' :
∀ {R : Type u} [inst : Ring R] (self : Subring R) {x : R}, x ∈ self.carrier → -x ∈ self.carrier
This theorem states that for any ring `R` and any subring `self` of `R`, if a certain element `x` is in the carrier of the subring, then the negation of `x` (denoted as `-x`) is also in the carrier of the subring. In other words, the subring `self` of a ring `R` is closed under the operation of negation.
More concisely: If `self` is a subring of a ring `R`, then for all `x` in `self`, we have `-x` in `self`. (In other words, `self` is closed under negation.)
|
Subring.zero_mem
theorem Subring.zero_mem : ∀ {R : Type u} [inst : Ring R] (s : Subring R), 0 ∈ s
This theorem states that for any given ring `R`, the zero element of that ring is always a member of any subring `s` of `R`. In other words, it confirms that zero, which is an identity element of addition in the ring, is also included in all of its subrings, in accordance with the definition of a subring in ring theory.
More concisely: For any subring `s` of a ring `R`, the additive identity (zero) of `R` is an element of `s`.
|