NonUnitalSubring.closure_le
theorem NonUnitalSubring.closure_le :
∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {s : Set R} {t : NonUnitalSubring R},
NonUnitalSubring.closure s ≤ t ↔ s ⊆ ↑t
The theorem `NonUnitalSubring.closure_le` states that for any type `R` equipped with a structure of a non-unital, non-associative ring, and any set `s` of elements of `R` and a NonUnitalSubring `t` of `R`, the non-unital subring generated by `s` is a subring of `t` if and only if `s` is a subset of `t`. In other words, a non-unital subring `t` includes the non-unital subring generated by a set `s` exactly when it includes all elements of the set `s`.
More concisely: A non-unital subring `t` of a non-unital, non-associative ring `R` includes the non-unital subring generated by a set `s` if and only if `s` is a subset of `t`.
|
NonUnitalSubring.closure_eq
theorem NonUnitalSubring.closure_eq :
∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (s : NonUnitalSubring R), NonUnitalSubring.closure ↑s = s := by
sorry
The theorem states that for any non-unital, non-associative ring `R`, the closure of a non-unital subring `s` of `R` is equal to `s` itself. In other words, taking the closure of a non-unital subring does not add any additional elements.
More concisely: For any non-unital subring `s` of a non-unital, non-associative ring `R`, the closure of `s` equals `s`.
|
NonUnitalSubring.mul_mem
theorem NonUnitalSubring.mul_mem :
∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (s : NonUnitalSubring R) {x y : R}, x ∈ s → y ∈ s → x * y ∈ s := by
sorry
This theorem states that for any type `R` that is a non-unital, non-associative ring, a given non-unital subring `s` of `R` is closed under multiplication. In other words, if `x` and `y` are elements of `s`, then the product `x * y` is also an element of `s`.
More concisely: For any non-unital, non-associative ring `R` and its non-unital subring `s`, the product of any two elements `x` and `y` in `s` lies in `s`.
|
NonUnitalSubring.add_mem
theorem NonUnitalSubring.add_mem :
∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (s : NonUnitalSubring R) {x y : R}, x ∈ s → y ∈ s → x + y ∈ s := by
sorry
This theorem states that for any non-unital, non-associative ring `R`, and any non-unital subring `s` of `R`, if `x` and `y` are elements of `s`, then their sum `x + y` is also in `s`. In other words, the non-unital subring `s` is closed under the operation of addition.
More concisely: For any non-unital ring `R` and non-unital subring `s` of `R`, if `x, y` are in `s`, then `x + y` is also in `s`.
|
NonUnitalRingHom.eqOn_set_closure
theorem NonUnitalRingHom.eqOn_set_closure :
∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] {f g : R →ₙ+* S}
{s : Set R}, Set.EqOn (⇑f) (⇑g) s → Set.EqOn ⇑f ⇑g ↑(NonUnitalSubring.closure s)
The theorem `NonUnitalRingHom.eqOn_set_closure` states that if two ring homomorphisms, `f` and `g`, are equal on a set `s` of some type `R`, then they are also equal on the closure of `s` in the non-unital, non-associative ring of that type. In other words, if for every element `x` in set `s`, `f(x) = g(x)`, then this equality holds for every element in the smallest non-unital subring of `R` that contains `s`. Here, a ring homomorphism is a function that preserves the ring structure (addition and multiplication operations) between two rings.
More concisely: If ring homomorphisms $f$ and $g$ agree on a set $s$ in a non-unital, non-associative ring $R$, then they agree on the closure of $s$ in the subring generated by $s$.
|
NonUnitalSubring.list_sum_mem
theorem NonUnitalSubring.list_sum_mem :
∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (s : NonUnitalSubring R) {l : List R},
(∀ x ∈ l, x ∈ s) → l.sum ∈ s
This theorem states that for any type `R` that has a structure of a non-unital non-associative ring, any non-unital subring `s` of `R`, and any list `l` of elements from `R`, if every element of `l` belongs to `s`, then the sum of all elements in `l` also belongs to `s`. In the context of abstract algebra, it basically says that the sum of a list of elements in a certain non-unital subring remains within that subring.
More concisely: If `R` is a non-unital non-associative ring, `s` is a non-unital subring of `R`, and all elements in list `l` belong to `s`, then the sum of all elements in `l` belongs to `s`.
|
NonUnitalSubring.ext
theorem NonUnitalSubring.ext :
∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {S T : NonUnitalSubring R}, (∀ (x : R), x ∈ S ↔ x ∈ T) → S = T := by
sorry
This theorem, `NonUnitalSubring.ext`, asserts that given two non-unital subrings `S` and `T` of a non-unital, non-associative ring `R`, if every element `x` from the ring `R` belongs to `S` if and only if it belongs to `T`, then the subrings `S` and `T` are equal. In other words, two non-unital subrings are considered the same if they contain exactly the same elements.
More concisely: If two non-unital subrings of a ring contain the same elements, then they are equal.
|
NonUnitalSubring.mem_iSup_of_directed
theorem NonUnitalSubring.mem_iSup_of_directed :
∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {ι : Sort u_2} [hι : Nonempty ι] {S : ι → NonUnitalSubring 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 type `R` which forms a NonUnitalNonAssocRing, a directed Sup of `NonUnitalSubring`s of `R` is equivalent to the union of these `NonUnitalSubring`s. More precisely, an element `x` of type `R` belongs to the directed Sup of `NonUnitalSubring`s if and only if there exists an index `i` such that `x` is in the `NonUnitalSubring` at index `i`. Here, a family of `NonUnitalSubring`s is directed if and only if for any two `NonUnitalSubring`s in the family, there exists another `NonUnitalSubring` in the family that is equal to or larger than both. The theorem emphasizes that without the directedness assumption, the union of two `NonUnitalSubring`s is typically not a `NonUnitalSubring`.
More concisely: For any non-unital, non-associative ring `R`, the directed supremum of a family of non-unital subrings of `R` equals the union of these subrings.
|
NonUnitalSubring.neg_mem'
theorem NonUnitalSubring.neg_mem' :
∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (self : NonUnitalSubring R) {x : R},
x ∈ self.carrier → -x ∈ self.carrier
This theorem states that for any type `R` that has a structure of `NonUnitalNonAssocRing` (a ring that is not necessarily unital or associative), and for any `NonUnitalSubring` of `R`, if an element `x` belongs to the carrier set of this subring, then its negation `-x` also belongs to this carrier set. In other words, this is a property that says that a non-unital, non-associative subring is closed under negation.
More concisely: For any non-unital, non-associative ring `R` and its non-unital subring, if an element `x` lies in the subring, then its negation `-x` also lies in the subring.
|
NonUnitalRingHom.map_closure
theorem NonUnitalRingHom.map_closure :
∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] (f : R →ₙ+* S)
(s : Set R), NonUnitalSubring.map f (NonUnitalSubring.closure s) = NonUnitalSubring.closure (⇑f '' s)
This theorem states that for any non-unital non-associative rings `R` and `S`, and any ring homomorphism `f` from `R` to `S`, the image under `f` of the non-unital subring generated by a set `s` in `R` equals the non-unital subring generated by the image of the set `s` in `S`. In mathematical terms, if `s` is a subset of `R` and `f: R →ₙ+* S` is a ring homomorphism, then the image of the subring generated by `s` under `f` is the same as the subring generated by the image of `s` under `f`.
More concisely: For any ring homomorphism $f$ from a non-unital ring $R$ to a non-unital ring $S$ and any subset $s$ of $R$, the image under $f$ of the subring generated by $s$ equals the subring generated by $f(s)$.
|
NonUnitalSubring.multiset_sum_mem
theorem NonUnitalSubring.multiset_sum_mem :
∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (s : NonUnitalSubring R) (m : Multiset R),
(∀ a ∈ m, a ∈ s) → m.sum ∈ s
This theorem states that for any type `R` that has a structure of a non-unital, non-associative ring, if `s` is a non-unital subring of `R` and `m` is a multiset of elements in `R`, then if all elements of `m` belong to `s`, the sum of the elements of `m` also belongs to `s`. Put another way, the sum of a multiset of elements from a non-unital subring of a non-unital, non-associative ring remains in the non-unital subring.
More concisely: For any non-unital, non-associative ring `R`, if `s` is a non-unital subring and `m` is a multiset of elements in `s`, then the sum of `m` belongs to `s`.
|
NonUnitalSubring.subset_closure
theorem NonUnitalSubring.subset_closure :
∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {s : Set R}, s ⊆ ↑(NonUnitalSubring.closure s)
This theorem states that for any type `R` that forms a Non-Unitary Non-Associative Ring, and any set `s` of elements of this type `R`, the set `s` is a subset of the Non-Unitary Subring generated by `s`. In other words, all elements in `s` are included in the Non-Unitary Subring that is created by taking `s` as a generating set.
More concisely: For any non-unitary, non-associative ring `R` and set `s` of its elements, `s` is a subset of the non-unitary subring generated by `s`.
|
Mathlib.RingTheory.NonUnitalSubring.Basic._auxLemma.10
theorem Mathlib.RingTheory.NonUnitalSubring.Basic._auxLemma.10 :
∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (x : R), (x ∈ ⊤) = True
This theorem states that for any type `R` that forms a non-unital, non-associative ring, any element `x` of `R` is an element of the top-level (or universal) subring. In the language of set theory, it states that the set of all elements in `R` is a subset of the universal subring, represented by ⊤.
More concisely: In any non-unital, non-associative ring `R`, every element `x` in `R` is contained in the universal subring ⊤.
|
NonUnitalSubring.closure_induction₂
theorem NonUnitalSubring.closure_induction₂ :
∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {s : Set R} {p : R → R → Prop} {a b : R},
a ∈ NonUnitalSubring.closure s →
b ∈ NonUnitalSubring.closure s →
(∀ x ∈ s, ∀ y ∈ s, p x y) →
(∀ (x : R), p 0 x) →
(∀ (x : R), p x 0) →
(∀ (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, also known as the Induction Principle for Closure Membership, applies to a set `s` of elements from a non-unital, non-associative ring `R`. The theorem states that for all `a, b` in the closure of `s` and for a binary predicate `p`, if `p` holds for all pairs of elements in `s`, `p` holds for `0` and any element in `R`, `p` is invariant under negation in either argument, `p` is preserved under addition in either argument, and `p` is preserved under multiplication in either argument, then `p` must also hold for the pair `a, b`.
In simpler terms, it demonstrates that if a property `p` is true for all elements in a set `s`, and this property behaves well under the operations of a non-unital, non-associative ring (like addition, negation, and multiplication), then this property is also true for all elements in the closure of `s`.
More concisely: If a property `p` holds for all elements in a set `s` of a non-unital, non-associative ring and is invariant under negation and preserved under addition and multiplication, then `p` holds for all elements in the closure of `s`.
|
NonUnitalSubring.sum_mem
theorem NonUnitalSubring.sum_mem :
∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (s : NonUnitalSubring R) {ι : Type u_2} {t : Finset ι}
{f : ι → R}, (∀ c ∈ t, f c ∈ s) → (t.sum fun i => f i) ∈ s
This theorem states that for any type `R` that is a non-unital non-associative ring, any `NonUnitalSubring` `s` of that ring, any finite set `t` of indices of type `ι`, and any function `f` from `ι` to `R`, if every element `c` in `t` maps to an element in the `NonUnitalSubring` `s` under the function `f`, then the sum of the elements in `t` mapped through the function `f` is also in the `NonUnitalSubring` `s`.
More concisely: If `R` is a non-unital non-associative ring, `s` is a non-unital subring of `R`, `t` is a finite set, and `f : ι -> R` maps `t` into `s`, then the sum of `f``(i)` for all `i` in `t` is also in `s`.
|
NonUnitalRingHom.range_top_of_surjective
theorem NonUnitalRingHom.range_top_of_surjective :
∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] (f : R →ₙ+* S),
Function.Surjective ⇑f → f.range = ⊤
The theorem `NonUnitalRingHom.range_top_of_surjective` states that for any types `R` and `S` which are instances of a non-unital non-associative ring, if there is a surjective ring homomorphism (a function respecting both addition and multiplication) `f` from `R` to `S`, then the range of `f` is the whole codomain `S`. In other words, for every element in `S`, there exists an element in `R` such that applying the function `f` to this element from `R` gives the element in `S`.
More concisely: If `R` and `S` are non-unital non-associative rings and `f` is a surjective ring homomorphism from `R` to `S`, then the range of `f` equals `S`.
|
NonUnitalSubring.closure_induction'
theorem NonUnitalSubring.closure_induction' :
∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {s : Set R} {p : ↥(NonUnitalSubring.closure s) → Prop}
(a : ↥(NonUnitalSubring.closure s)),
(∀ (x : R) (hx : x ∈ s), p ⟨x, ⋯⟩) →
p 0 →
(∀ (x y : ↥(NonUnitalSubring.closure s)), p x → p y → p (x + y)) →
(∀ (x : ↥(NonUnitalSubring.closure s)), p x → p (-x)) →
(∀ (x y : ↥(NonUnitalSubring.closure s)), p x → p y → p (x * y)) → p a
The theorem `NonUnitalSubring.closure_induction'` asserts that for any type `R` that forms a non-unital, non-associative ring, any set of elements `s` from `R`, and any property `p` acting on the elements of the non-unital subring closure of `s`, if the property holds for each element in `s`, the zero element, the sum of any two elements, the negative of any element, and the product of any two elements in the closure, then it holds for all elements in the closure.
In mathematical language, given a non-unital, non-associative ring `R`, a set `s` of `R`, and a property `p` that is applied to the elements of the closure of `s` (as a non-unital subring), if `p` is valid for each `x ∈ s`, for `0`, for `x + y`, `-x`, and `x * y` where `x` and `y` are any elements in the closure, then `p` is valid for all elements in the closure.
More concisely: If `R` is a non-unital, non-associative ring, `s` is a set of `R`, and `p` is a property that holds for all elements in `s`, zero, the sum and difference of any two elements, and the product of any two elements in the non-unital subring closure of `s`, then `p` holds for all elements in the closure.
|
NonUnitalRingHom.mem_range
theorem NonUnitalRingHom.mem_range :
∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] {f : R →ₙ+* S}
{y : S}, y ∈ f.range ↔ ∃ x, f x = y
This theorem states that, given non-unital non-associative rings `R` and `S`, any ring homomorphism `f : R →ₙ+* S`, and any element `y` in `S`, `y` is in the range of `f` if and only if there exists an element `x` in `R` such that applying the ring homomorphism `f` to `x` produces `y`. This theorem essentially defines the range of a ring homomorphism in terms of the algebraic structures and the mapping it embodies.
More concisely: A ring homomorphism maps an element in its domain to an element in its range if and only if there exists a corresponding element in the domain that maps to it under the homomorphism.
|
NonUnitalSubring.zero_mem
theorem NonUnitalSubring.zero_mem : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (s : NonUnitalSubring R), 0 ∈ s
This theorem states that for any non-unital, non-associative ring `R`, zero (denoted as `0`) is an element of any non-unital subring `s` of `R`. Essentially, this is telling us that the zero element of the ring is always included in its non-unital subrings.
More concisely: In any non-unital ring, the additive identity (zero) belongs to every non-unital subring.
|
NonUnitalSubring.gc_map_comap
theorem NonUnitalSubring.gc_map_comap :
∀ {F : Type w} {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S]
[inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (f : F),
GaloisConnection (NonUnitalSubring.map f) (NonUnitalSubring.comap f)
The theorem `NonUnitalSubring.gc_map_comap` states that for all types `F`, `R`, `S`, where `R` and `S` are non-unital non-associative rings, `F` is a function-like object from `R` to `S`, and `F` forms a non-unital ring homomorphism between `R` and `S`; for any term `f` of type `F`, there is a Galois connection between the `map` operation and `comap` operation on non-unital subrings induced by `f`. In other words, for any two subrings `a` of `R` and `b` of `S`, `a` is mapped to a subring less than or equal to `b` if and only if `a` is less than or equal to the preimage of `b` under the homomorphism `f`.
More concisely: For any non-unital non-associative rings R, S, and a function-like object F from R to S that is a non-unital ring homomorphism, there is a Galois connection between the map and comap operations on non-unital subrings of R and S induced by F.
|
NonUnitalSubring.sub_mem
theorem NonUnitalSubring.sub_mem :
∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (s : NonUnitalSubring R) {x y : R}, x ∈ s → y ∈ s → x - y ∈ s := by
sorry
This theorem states that for any non-unital non-associative ring `R` and any non-unital subring `s` of `R`, if `x` and `y` are elements of `s`, then the difference `x - y` is also an element of `s`. In other words, a non-unital subring is closed under the operation of subtraction.
More concisely: In a non-unital ring, any non-unital subring is closed under subtraction. That is, for any non-unital rings `R` and subring `s` of `R`, and for any `x, y` in `s`, `x - y` is also in `s`.
|
NonUnitalSubring.neg_mem
theorem NonUnitalSubring.neg_mem :
∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (s : NonUnitalSubring R) {x : R}, x ∈ s → -x ∈ s
This theorem states that for any type `R` that is a non-unital, non-associative ring, and for any non-unital subring `s` of `R`, if an element `x` is in `s`, then its negation `-x` is also in `s`. In simpler terms, if you have a non-unital subring (which is a certain type of mathematical structure), then it remains closed under the operation of negation.
More concisely: For any non-unital, non-associative ring R and its non-unital subring s, if x ∈ s then -x ∈ s.
|
NonUnitalSubring.closure_induction
theorem NonUnitalSubring.closure_induction :
∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {s : Set R} {p : R → Prop} {x : R},
x ∈ NonUnitalSubring.closure s →
(∀ x ∈ s, p x) →
p 0 →
(∀ (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, `NonUnitalSubring.closure_induction`, provides an induction principle for membership in the closure of a set `s` under the context of a non-unital non-associative ring `R`. It states that for any ring element `x` and a property `p` on elements of `R`, if `x` is in the closure of `s`, `p` holds for all elements of `s`, `p` is true for the additive identity `0` and `1`, `p` is preserved under addition, negation and multiplication of any two elements of `R`, then `p` is also true for `x`. In simpler terms, if a property holds for `0`, `1`, all elements in a set, and is preserved under the ring operations, then it holds for all elements in the closure of the set in a non-unital non-associative ring context.
More concisely: In a non-unital non-associative ring, if a property holds for 0, 1, and all elements in a set, and is preserved under addition, negation, and multiplication, then the property holds for all elements in the closure of the set.
|
NonUnitalSubring.mk'.proof_2
theorem NonUnitalSubring.mk'.proof_2 :
∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (s : Set R) (sa : AddSubgroup R), ↑sa = s → s = ↑sa
This theorem states that for any type `R` that is a non-unital non-associative ring, and for any set `s` of elements of `R` and any additive subgroup `sa` of `R`, if `s` is identical to the set of elements in the subgroup `sa` (expressed as `↑sa = s`), then the reverse is also true: the set `s` is identical to the set of elements in the subgroup `sa` (expressed as `s = ↑sa`). This asserts that the equality between a set and a subgroup in a non-unital non-associative ring is symmetric, i.e., if one can be cast to the other, the reverse is also true.
More concisely: In a non-unital non-associative ring, if the set `s` is equal to the subgroup `sa` generated by `s`, then `s` is equal to its subgroup generator `sa`.
|
NonUnitalSubring.closure_mono
theorem NonUnitalSubring.closure_mono :
∀ {R : Type u} [inst : NonUnitalNonAssocRing R] ⦃s t : Set R⦄,
s ⊆ t → NonUnitalSubring.closure s ≤ NonUnitalSubring.closure t
The theorem `NonUnitalSubring.closure_mono` asserts that the operation of taking the `NonUnitalSubring` closure of a set is monotone with respect to set inclusion. In other words, given any type `R` equipped with a `NonUnitalNonAssocRing` structure, and any two sets `s` and `t` of elements of `R`, if `s` is a subset of `t` (`s ⊆ t`), then the `NonUnitalSubring` closure of `s` is a subring of or equal to the `NonUnitalSubring` closure of `t` (`NonUnitalSubring.closure s ≤ NonUnitalSubring.closure t`).
More concisely: The `NonUnitalSubring.closure` operation on sets of elements of a `NonUnitalNonAssocRing` `R` is monotone with respect to set inclusion, i.e., `NonUnitalSubring.closure s ≤ NonUnitalSubring.closure t` for any `s ⊆ t`.
|