RingHom.coe_rangeS
theorem RingHom.coe_rangeS :
∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S),
↑f.rangeS = Set.range ⇑f
This theorem states that for all types `R` and `S` which are non-associative semirings, and for every ring homomorphism `f` from `R` to `S`, the co-domain of the homomorphism when considered as a subsemiring (`RingHom.rangeS f`) is precisely the set of all elements in `S` that can be obtained by applying `f` to some element of `R` (`Set.range ⇑f`). In other words, it establishes the equivalence between the range of the ring homomorphism as a subsemiring and the set of values it can take.
More concisely: For every non-associative semirings `R` and `S` and ring homomorphism `f` from `R` to `S`, `RingHom.rangeS f` equals `Set.range (f : R → S)`.
|
Subsemiring.one_mem
theorem Subsemiring.one_mem : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R), 1 ∈ s
This theorem states that for any given type `R` that has a structure of a non-associative semiring, the multiplicative identity (1) of the semiring is always an element of any subsemiring `s` of `R`. Thus, the structure of a subsemiring always inherits the multiplicative identity from its parent semiring.
More concisely: For any non-associative semiring `R` and subsemiring `s` of `R`, the multiplicative identity of `R` is an element of `s`.
|
coe_nat_mem
theorem coe_nat_mem :
∀ {S : Type u_1} {R : Type u_2} [inst : AddMonoidWithOne R] [inst_1 : SetLike S R] (s : S)
[inst_2 : AddSubmonoidWithOneClass S R] (n : ℕ), ↑n ∈ s
This theorem states that for any types `R` and `S` where `R` is a Non-Associative Semiring and `S` is a set-like structure over `R` exhibiting the behavior of a subsemiring, the natural number coercion of any natural number `n` belongs to the set `s` of type `S`. In other words, if you cast a natural number to the semiring `R` and then put it in a subsemiring `s` of `R`, it will always be in `s`.
More concisely: For any non-associative semiring R and subsemiring s of R as a set-like structure, the natural number coercion of any natural number belongs to s.
|
RingHom.rangeS_top_of_surjective
theorem RingHom.rangeS_top_of_surjective :
∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S),
Function.Surjective ⇑f → f.rangeS = ⊤
The theorem `RingHom.rangeS_top_of_surjective` states that for any two types `R` and `S`, given that both `R` and `S` are non-associative semirings, if there exists a ring homomorphism `f` from `R` to `S` that is surjective (i.e., for every element `b` in `S`, there is some element `a` in `R` such that `f(a) = b`), then the range of `f`, as defined by `RingHom.rangeS`, is the entire codomain `S` (denoted by `⊤`). In other words, a surjective ring homomorphism maps to every element in the codomain.
More concisely: A surjective ring homomorphism between non-associative semirings maps the entire domain to the entire codomain.
|
RingHom.eqOn_sclosure
theorem RingHom.eqOn_sclosure :
∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {f g : R →+* S} {s : Set R},
Set.EqOn (⇑f) (⇑g) s → Set.EqOn ⇑f ⇑g ↑(Subsemiring.closure s)
This theorem states that if two ring homomorphisms, `f` and `g`, are equal on a set `s` of elements from a non-associative semiring `R`, then these two homomorphisms are also equal on the closure of `s` under the operations of `R`. In this context, the closure of `s` is the smallest subsemiring of `R` that includes `s`. A ring homomorphism is a function that preserves the ring operations (addition and multiplication), and 'equal on a set' means that `f(x) = g(x)` for all `x` in that set.
More concisely: If two ring homomorphisms agree on a set, they agree on its closure under the semiring operations.
|
Subsemiring.sum_mem
theorem Subsemiring.sum_mem :
∀ {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R) {ι : Type u_1} {t : Finset ι} {f : ι → R},
(∀ c ∈ t, f c ∈ s) → (t.sum fun i => f i) ∈ s
The theorem `Subsemiring.sum_mem` states that for any type `R` that is a non-associative semiring, and any subsemiring `s` of `R`, if you have a function `f` from an index type `ι` to `R` such that for every element `c` in a finite set `t` of type `ι`, `f(c)` is an element of `s`, then the sum of the function `f` evaluated at each element of `t` is also an element of the subsemiring `s`. In mathematical terms, if all elements of a finite sum are in a subsemiring, then the sum itself is also in that subsemiring.
More concisely: If `f : ι -> R` is a function with finite domain such that for all `c in ι`, `f(c)` belongs to a subsemiring `s` of non-associative semiring `R`, then the sum of `{f(c) | c in finite set t}` belongs to `s`.
|
Subsemiring.prod_mem
theorem Subsemiring.prod_mem :
∀ {R : Type u_1} [inst : CommSemiring R] (s : Subsemiring 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 given commutative semiring `R`, a subsemiring `s` of `R`, a finite set `t` indexed by type `ι`, and a function `f` mapping from `ι` to `R`, if every element `c` in `t` maps to an element in the subsemiring `s` via `f`, then the product of all elements in `t` (each transformed by the function `f`) also belongs to the same subsemiring `s`. Here, the product operation is as defined for the commutative semiring `R`.
More concisely: If `f : ι → R` maps a finite set `t ⊆ R` to a subsemiring `s ≤ R` such that for all `c ∈ t`, `f(c) ∈ s`, then `∏(f `` t) ∈ s`, where `∏` denotes the product operation in `R`.
|
Subsemiring.coe_closure_eq
theorem Subsemiring.coe_closure_eq :
∀ {R : Type u} [inst : NonAssocSemiring R] (s : Set R),
↑(Subsemiring.closure s) = ↑(AddSubmonoid.closure ↑(Submonoid.closure s))
This theorem states that for any set `s` of elements in a non-associative semiring `R`, the elements of the subsemiring generated by `s` are exactly the same as the elements of the additive closure of the multiplicative submonoid generated by `s`. In other words, the process of generating a subsemiring, starting from a set and subsequently creating a subsemiring, produces the same set of elements as starting with the same set, generating a multiplicative submonoid and then taking its additive closure.
More concisely: The subsemiring generated by a set in a non-associative semiring is equal to the additive closure of the multiplicative submonoid generated by that set.
|
Subsemiring.zero_mem'
theorem Subsemiring.zero_mem' : ∀ {R : Type u} [inst : NonAssocSemiring R] (self : Subsemiring R), 0 ∈ self.carrier
This theorem states that for any type `R` that is a non-associative semiring and for any subsemiring `self` of `R`, the element `0` is a member of the carrier set of `self`. In other words, every additive submonoid of a non-associative semiring includes the element `0`.
More concisely: In any non-associative semiring, the additive identity (0) belongs to every subsemiring.
|
Subsemiring.add_mem
theorem Subsemiring.add_mem :
∀ {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R) {x y : R}, x ∈ s → y ∈ s → x + y ∈ s
This theorem states that a subsemiring is closed under addition. In other words, for any type `R` that forms a non-associative semiring, if `s` is a subsemiring of `R`, and `x` and `y` are elements of `s`, then the sum of `x` and `y` is also an element of `s`.
More concisely: If `s` is a subsemiring of the non-associative semiring `R`, then for all `x, y ∈ s`, `x + y ∈ s`.
|
Subsemiring.subset_closure
theorem Subsemiring.subset_closure :
∀ {R : Type u} [inst : NonAssocSemiring R] {s : Set R}, s ⊆ ↑(Subsemiring.closure s)
This theorem states that for any type `R` equipped with a non-associative semiring structure, and any set `s` of elements of type `R`, the set `s` is included in the subsemiring generated by `s`. In other words, every element of `s` is also an element of the subsemiring generated by `s`. This is a typical property of closures, where the closure of a set (in this case, the subsemiring closure) always contains the original set.
More concisely: For any non-associative semiring `R` and set `s` of elements in `R`, `s` is included in the subsemiring generated by `s`.
|
Subsemiring.multiset_sum_mem
theorem Subsemiring.multiset_sum_mem :
∀ {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R) (m : Multiset R), (∀ a ∈ m, a ∈ s) → m.sum ∈ s := by
sorry
This theorem states that the sum of a multiset of elements, all of which belong to a specific subsemiring 's' of a semiring 'R', also belongs to the same subsemiring 's'. Here, a semiring is a non-associative semiring, a multiset is a collection of items that allows for multiple occurrences of the same element, and a subsemiring is a subset that retains the algebraic structure of the original semiring. The sum of the multiset is calculated in the context of this semiring. This theorem is valid for any type 'R' that forms a non-associative semiring, any subsemiring 's' of 'R', and any multiset 'm' of elements of 'R'.
More concisely: Given a non-associative semiring R, a subsemiring s of R, and a multiset m of elements from R, the sum of the elements in m, calculated in the context of s, belongs to s.
|
Subsemiring.closure_eq
theorem Subsemiring.closure_eq :
∀ {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R), Subsemiring.closure ↑s = s
The theorem `Subsemiring.closure_eq` states that for any subset `s` of a type `R` with a non-associative semiring structure, the closure of `s` in the sense of subsemirings equals `s` itself. In other words, if `s` is a subsemiring of a non-associative semiring `R`, then the smallest subsemiring of `R` that contains `s` (the closure of `s`) is `s`. This expresses the property that `s` is already a closed subsemiring.
More concisely: The theorem `Subsemiring.closure_eq` asserts that in a non-associative semiring, a subset is equal to its own closure as a subsemiring.
|
Subsemiring.closure_le
theorem Subsemiring.closure_le :
∀ {R : Type u} [inst : NonAssocSemiring R] {s : Set R} {t : Subsemiring R}, Subsemiring.closure s ≤ t ↔ s ⊆ ↑t := by
sorry
This theorem states that, for any type `R` with the structure of a nonassociative semiring, and any set `s` of elements of `R` and any subsemiring `t` of `R`, the subsemiring generated by `s` (denoted as `Subsemiring.closure s`) is a subset of `t` if and only if `s` is a subset of `t`. In other words, a subsemiring `t` includes the smallest possible subsemiring `Subsemiring.closure s` which includes all elements of `s` if and only if `t` includes all elements of `s` directly.
More concisely: For any nonassociative semiring `R`, set `s` of elements in `R`, and subsemiring `t` of `R`, `Subsemiring.closure s ⊆ t` if and only if `s ⊆ t`.
|
Subsemiring.closure_induction
theorem Subsemiring.closure_induction :
∀ {R : Type u} [inst : NonAssocSemiring R] {s : Set R} {p : R → Prop} {x : R},
x ∈ Subsemiring.closure s →
(∀ x ∈ s, p x) →
p 0 → p 1 → (∀ (x y : R), p x → p y → p (x + y)) → (∀ (x y : R), p x → p y → p (x * y)) → p x
This theorem, named `Subsemiring.closure_induction`, states an induction principle for membership in the closure of a set in a non-associative semiring. Given any type `R` that forms a non-associative semiring, a set `s` of elements of that type, a property `p` that may hold for elements of `R`, and an element `x` of `R`, if `x` is in the subsemiring generated by the closure of `s`, then the following conditions imply that `p` holds for `x`:
* `p` holds for every element in `s`
* `p` holds for `0`
* `p` holds for `1`
* `p` is preserved under addition, meaning that for any two elements `x` and `y` in `R`, if `p` holds for `x` and `y`, then `p` holds for their sum `x + y`
* `p` is preserved under multiplication, meaning that for any two elements `x` and `y` in `R`, if `p` holds for `x` and `y`, then `p` holds for their product `x * y`.
In simpler terms, if a property holds for all elements in a set, and also holds for the zero and one elements, and is maintained when adding or multiplying any two elements for which the property holds, then this property holds for all elements in the subsemiring generated by the closure of the initial set.
More concisely: If `s` is a set in a non-associative semiring `R`, `p` is a property that holds for all elements in `s`, `0`, and `1`, and is preserved under addition and multiplication, then `p` holds for every element in the subsemiring generated by the closure of `s`.
|
Subsemiring.ext
theorem Subsemiring.ext :
∀ {R : Type u} [inst : NonAssocSemiring R] {S T : Subsemiring R}, (∀ (x : R), x ∈ S ↔ x ∈ T) → S = T
This theorem states that two subsemirings `S` and `T` of a non-associative semiring `R` are equal if they possess the same elements. In other words, if every element `x` in `R` that is in subsemiring `S` is also in subsemiring `T` and vice versa, then the subsemirings `S` and `T` are indeed the same.
More concisely: If two subsemirings `S` and `T` of a non-associative semiring `R` have the same elements, then `S = T`.
|
RingHom.mem_rangeS
theorem RingHom.mem_rangeS :
∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {f : R →+* S} {y : S},
y ∈ f.rangeS ↔ ∃ x, f x = y
This theorem states that for any types `R` and `S`, which are both non-associative semirings, and any ring homomorphism `f` from `R` to `S`, and any element `y` of `S`, `y` is in the range of the ring homomorphism `f` if and only if there exists an element `x` in `R` such that applying the function `f` to `x` gives `y`.
More concisely: For any non-associative semirings R and S, and ring homomorphism f from R to S, y ∈ Im(f) if and only if there exists x ∈ R such that f(x) = y.
|
Subsemiring.list_sum_mem
theorem Subsemiring.list_sum_mem :
∀ {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R) {l : List R}, (∀ x ∈ l, x ∈ s) → l.sum ∈ s := by
sorry
This theorem states that the sum of all elements in a list, where each element is within a particular subsemiring, is also in that same subsemiring. Here, 'R' represents any type that forms a non-associative semiring, 's' represents a subsemiring of 'R', and 'l' is a list of elements of type 'R'. The condition (∀ x ∈ l, x ∈ s) ensures that every element of the list 'l' is in the subsemiring 's'.
More concisely: The sum of all elements in a list of a non-associative semiring is in the same subsemiring if every element of the list belongs to the subsemiring.
|
Subsemiring.mul_mem
theorem Subsemiring.mul_mem :
∀ {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R) {x y : R}, x ∈ s → y ∈ s → x * y ∈ s
This theorem states that for any non-associative semiring `R` and any subsemiring `s` of `R`, if elements `x` and `y` belong to `s`, then their multiplication `x * y` also belongs to `s`. In other words, a subsemiring is closed under the operation of multiplication.
More concisely: In any non-associative semiring, the product of two elements from a subsemiring lies in the subsemiring.
|
Subsemiring.multiset_prod_mem
theorem Subsemiring.multiset_prod_mem :
∀ {R : Type u_1} [inst : CommSemiring R] (s : Subsemiring R) (m : Multiset R), (∀ a ∈ m, a ∈ s) → m.prod ∈ s := by
sorry
This theorem states that for any type `R` that is a commutative semiring, and any subsemiring `s` of `R`, the product of a multiset of elements `m` from `R` is in `s`, given that all elements `a` in `m` are in `s`. In other words, if we have a collection (multiset) of elements from a subsemiring of a commutative semiring, the product of all these elements will still belong to the same subsemiring.
More concisely: If `R` is a commutative semiring and `s` is a subsemiring of `R`, then the product of any multiset of elements from `s` is in `s`.
|
Subsemiring.zero_mem
theorem Subsemiring.zero_mem : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R), 0 ∈ s
This theorem states that for any given subsemiring `s` of a non-associative semiring `R`, the element `0` from the semiring `R` is contained in the subsemiring `s`. In other words, the zero element of a semiring is always an element of any of its subsemirings.
More concisely: For any subsemiring `s` of a semiring `R`, the additive identity of `R` is an element of `s`.
|
Subsemiring.list_prod_mem
theorem Subsemiring.list_prod_mem :
∀ {R : Type u_1} [inst : Semiring R] (s : Subsemiring R) {l : List R}, (∀ x ∈ l, x ∈ s) → l.prod ∈ s
This theorem states that for any given type `R` that constitutes a semiring, and any subsemiring `s` of `R`, if all elements of a list `l` of type `R` are in `s`, then the product of all elements in the list `l` is also in the subsemiring `s`. In mathematical terms, for a semiring `(R, +, *)` and a subsemiring `s`, if all elements `x` of a list `l` belong to the set `s`, then the product of all elements in `l` lies within `s` as well.
More concisely: If `R` is a semiring and `s` is a subsemiring of `R` such that all elements of a list `l` in `R` belong to `s`, then the product of all elements in `l` belongs to `s`.
|
Subsemiring.closure_mono
theorem Subsemiring.closure_mono :
∀ {R : Type u} [inst : NonAssocSemiring R] ⦃s t : Set R⦄, s ⊆ t → Subsemiring.closure s ≤ Subsemiring.closure t
The theorem `Subsemiring.closure_mono` states that, for any type `R` that is a non-associative semiring, and for any two sets `s` and `t` of `R`, if `s` is a subset of `t`, then the subsemiring generated by `s` is a subsemiring of (or equal to) the subsemiring generated by `t`. In mathematical terms, if `s ⊆ t`, then the closure of `s` under the subsemiring operation is contained within or equal to the closure of `t` under the same operation. This demonstrates the monotonicity of the subsemiring closure operation with respect to set inclusion.
More concisely: If `R` is a non-associative semiring and `s` is a subset of `t`, then the subsemiring generated by `s` is contained in or equal to the subsemring generated by `t`.
|
Submonoid.subsemiringClosure_eq_closure
theorem Submonoid.subsemiringClosure_eq_closure :
∀ {R : Type u} [inst : NonAssocSemiring R] (M : Submonoid R), M.subsemiringClosure = Subsemiring.closure ↑M := by
sorry
This theorem states that for any type `R` which forms a non-associative semiring, and any multiplicative submonoid `M` of `R`, the subsemiring generated by `M` is identical to the closure of the set formed by `M` in the subsemiring. In other words, the subsemiring created by the submonoid `M` is the smallest subsemiring that contains every element of `M`.
More concisely: Let `R` be a non-associative semiring and `M` a multiplicative submonoid of `R`. The subsemiring generated by `M` equals the closure of `M` in `R`.
|
Subsemiring.gc_map_comap
theorem Subsemiring.gc_map_comap :
∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S),
GaloisConnection (Subsemiring.map f) (Subsemiring.comap f)
This theorem states that for any two types `R` and `S` that are non-associative semirings, and any ring homomorphism `f` from `R` to `S`, there exists a Galois connection between the operation of mapping a subsemiring of `R` along `f` and the operation of getting the preimage of a subsemiring of `S` along `f`. In other words, if we use `f` to map a subsemiring of `R` to `S`, and then map back to `R` via the preimage, we will maintain a certain order relation. This order relation is defined by the Galois connection: the image of a subsemiring under `f` is less than or equal to a subsemiring in `S` if and only if the original subsemiring is less than or equal to the preimage of the subsemiring in `S` under `f`. This connection is a fundamental property in order theory and category theory.
More concisely: Given any non-associative semirings `R` and `S` and a ring homomorphism `f` from `R` to `S`, there exists a Galois connection between the mapping of subsemirings of `R` along `f` and the mapping of preimages of subsemirings of `S` along `f`, such that for all subsemirings `X` of `R` and `Y` of `S`, `f(X) ⊆ Y` if and only if `X ⊆ f⁻¹(Y)`.
|
RingHom.map_closureS
theorem RingHom.map_closureS :
∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S) (s : Set R),
Subsemiring.map f (Subsemiring.closure s) = Subsemiring.closure (⇑f '' s)
The theorem `RingHom.map_closureS` states that for any two types `R` and `S` that are both non-associative semirings, and for any ring homomorphism `f` from `R` to `S`, and any set `s` of elements of `R`, if we take the subsemiring generated by `s` in `R`, and map it to `S` using `f`, we obtain the same result as if we took the image of `s` under `f` and then took the subsemiring generated by this image in `S`. In mathematical terms, this theorem establishes that the image under a ring homomorphism of the subsemiring generated by a set equals the subsemiring generated by the image of the set.
More concisely: For any non-associative semirings R and S, ring homomorphism f from R to S, and subset s of R, the image under f of the subsemiring generated by s is equal to the subsemiring generated by the image of s in S.
|
Subsemiring.closure_induction₂
theorem Subsemiring.closure_induction₂ :
∀ {R : Type u} [inst : NonAssocSemiring R] {s : Set R} {p : R → R → Prop} {x y : R},
x ∈ Subsemiring.closure s →
y ∈ Subsemiring.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₁ 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 x y
This theorem, `Subsemiring.closure_induction₂`, provides an induction principle for proving properties about elements within the closure of a subsemiring generated by a set in a non-associative semiring. The theorem states that for any type `R` with a non-associative semiring structure, any set `s` in `R`, and a predicate function `p` accepting two arguments from `R`, if `x` and `y` are elements of the closure of `s`, and the predicate holds for all pairs of elements in `s`, for all pairs where one of the components is `0` or `1`, and remains true under addition and multiplication operations, then the predicate holds for `x` and `y`. Essentially, this theorem allows us to show that a property, which holds in the generating set and is preserved under semiring operations, extends to all elements of the closure.
More concisely: If `s` is a set in a non-associative semiring `R`, `p` is a predicate on `R` that holds for all pairs in `s` where one element is `0` or `1`, and is closed under addition and multiplication, then `p` holds for all pairs of elements in the closure of `s`.
|
Mathlib.RingTheory.Subsemiring.Basic._auxLemma.10
theorem Mathlib.RingTheory.Subsemiring.Basic._auxLemma.10 :
∀ {R : Type u} [inst : NonAssocSemiring R] (x : R), (x ∈ ⊤) = True
This theorem states that for any type `R` that forms a non-associative semiring, any element `x` of `R` belongs to the top element `⊤` (which represents the whole semiring). This is always true, regardless of the specific element `x` or the specifics of `R`. Essentially, in mathematical terms, it's saying that for any `x` in a given non-associative semiring, `x` is indeed an element of the entire semiring.
More concisely: For any non-associative semiring R, every element x in R belongs to the semiring's top element ⊤.
|
Subsemiring.add_mem'
theorem Subsemiring.add_mem' :
∀ {R : Type u} [inst : NonAssocSemiring R] (self : Subsemiring R) {a b : R},
a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
This theorem states that for any non-associative semiring `R` (a kind of algebraic structure), if `a` and `b` are elements of a subsemiring (a subset retaining the semiring operations) of `R`, then their sum `a + b` also belongs to this subsemiring. This property is a fundamental part of the definition of a subsemiring.
More concisely: In a non-associative semiring, if `a` and `b` belong to a subsemiring and `R` is the semiring, then `a + b` also belongs to the subsemiring.
|