NonUnitalSubsemiring.closure_mono
theorem NonUnitalSubsemiring.closure_mono :
∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] ⦃s t : Set R⦄,
s ⊆ t → NonUnitalSubsemiring.closure s ≤ NonUnitalSubsemiring.closure t
The theorem `NonUnitalSubsemiring.closure_mono` states that for any type `R` which has a non-unital non-associative semiring structure, the operation of taking the subsemiring closure of a set is monotone. In other words, for any two sets `s` and `t` of type `R`, if `s` is a subset of `t` (denoted as `s ⊆ t`), then the subsemiring closure of `s` is a subset of or equal to the subsemiring closure of `t` (denoted as `NonUnitalSubsemiring.closure s ≤ NonUnitalSubsemiring.closure t`). The subsemiring closure of a set is a mathematical operation that produces the smallest semiring that contains the set.
More concisely: For any non-unital non-associative semiring `R` and sets `s` and `t` of `R`, if `s ⊆ t`, then `NonUnitalSubsemiring.closure s ≤ NonUnitalSubsemiring.closure t`.
|
NonUnitalSubsemiring.ext
theorem NonUnitalSubsemiring.ext :
∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {S T : NonUnitalSubsemiring R},
(∀ (x : R), x ∈ S ↔ x ∈ T) → S = T
This theorem states that in the context of a non-unital, non-associative semiring `R`, two distinct non-unital subsemirings `S` and `T` of `R` are considered equal if they contain exactly the same elements. In other words, if every element `x` in semiring `R` satisfies the condition that it is in `S` if and only if it is in `T`, then `S` and `T` are the same subsemiring.
More concisely: In a non-unital, non-associative semiring, two distinct subsemirings are equal if and only if they contain the same elements.
|
NonUnitalRingHom.mem_srange
theorem NonUnitalRingHom.mem_srange :
∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
{F : Type u_1} [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] {f : F} {y : S},
y ∈ NonUnitalRingHom.srange f ↔ ∃ x, f x = y
The theorem `NonUnitalRingHom.mem_srange` states that for any types `R` and `S` that are instances of `NonUnitalNonAssocSemiring`, and any type `F` that is an instance of `FunLike F R S` and `NonUnitalRingHomClass F R S`, a value `y` of type `S` belongs to the range of a non-unital ring homomorphism `f : F` if and only if there exists a value `x` such that applying `f` to `x` yields `y`. In other words, the theorem establishes the exact condition under which a value can be said to be in the range of a non-unital ring homomorphism.
More concisely: A value in `S` is in the range of a non-unital ring homomorphism from `R` to `S` if and only if it is the image of some element in `R`.
|
NonUnitalSubsemiring.closure_induction₂
theorem NonUnitalSubsemiring.closure_induction₂ :
∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {s : Set R} {p : R → R → Prop} {x y : R},
x ∈ NonUnitalSubsemiring.closure s →
y ∈ NonUnitalSubsemiring.closure s →
(∀ x ∈ s, ∀ y ∈ s, p x y) →
(∀ (x : R), p 0 x) →
(∀ (x : R), p x 0) →
(∀ (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
The theorem `NonUnitalSubsemiring.closure_induction₂` is an induction principle for membership in the closure of a set under a non-unital, non-associative semiring operation, where the induction is performed on a two-argument predicate. Given a type `R` with a non-unital, non-associative semiring structure, a set `s` of elements of `R`, and a predicate `p` on pairs of elements of `R`, if we have that `x` and `y` are elements of the closure of `s`, and `p` is true for all pairs of elements in `s`, holds for the zero-element with any element, is preserved under addition and multiplication in both arguments, then `p` holds for `x` and `y`.
More concisely: If `s` is a set in the non-unital, non-associative semiring `R` such that for all `x, y in s` and `z in closure(s)`, `p(x, y)` holds, and `p` is preserves under addition and multiplication in both arguments, then `p(z, any x in R)` holds.
|
NonUnitalRingHom.eqOn_sclosure
theorem NonUnitalRingHom.eqOn_sclosure :
∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
{F : Type u_1} [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] {f g : F} {s : Set R},
Set.EqOn (⇑f) (⇑g) s → Set.EqOn ⇑f ⇑g ↑(NonUnitalSubsemiring.closure s)
This theorem states that, given two non-unital ring homomorphisms `f` and `g` from a type `R` to a type `S`, both of which have a non-unital non-associated semiring structure, and a set `s` of elements of type `R`, if `f` and `g` are equal on `s` (i.e., they map every element of `s` to the same value), then they are also equal on the closure of `s` under the structure of a non-unital subsemiring. This closure is the smallest non-unital subsemiring of `R` that contains `s`, and the equality of `f` and `g` on this closure means that for every element in the closure, `f` and `g` map it to the same value in `S`. In other words, if two non-unital ring homomorphisms agree on a set, they also agree on the smallest non-unital subsemiring that includes that set.
More concisely: Given two non-unital ring homomorphisms from a non-unital semiring to another, if they agree on a set and its closure under the non-unital subsemiring structure, then they are equal.
|
NonUnitalSubsemiring.closure_le
theorem NonUnitalSubsemiring.closure_le :
∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {s : Set R} {t : NonUnitalSubsemiring R},
NonUnitalSubsemiring.closure s ≤ t ↔ s ⊆ ↑t
This theorem states that for any type `R` with a structure of a non-unital, non-associative semiring, and any set `s` of elements of `R` and any non-unital subsemiring `t` of `R`, the non-unital subsemiring generated by `s` (denoted by `NonUnitalSubsemiring.closure s`) is contained in `t` if and only if every element of `s` is an element of `t`. In other words, a non-unital subsemiring includes the closure of a set if and only if it includes the set itself. This theorem hence provides a characterization of the closure of a set in terms of inclusion into non-unital subsemirings.
More concisely: For any non-unital semiring `R`, set `s` of its elements, and non-unital subsemiring `t`, `NonUnitalSubsemiring.closure s ⊆ t` if and only if `s ⊆ t`.
|
NonUnitalSubsemiring.closure_eq
theorem NonUnitalSubsemiring.closure_eq :
∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (s : NonUnitalSubsemiring R),
NonUnitalSubsemiring.closure ↑s = s
This theorem states that for any type `R` with an instance of a non-unital, non-associative semiring, and for any non-unital subsemiring `s` of `R`, the closure of `s` is equal to `s` itself. In other words, this theorem is asserting that the process of taking the closure of a non-unital subsemiring does not add any new elements to the subsemiring.
More concisely: For any non-unital, non-associative semiring `R` and its non-unital subsemiring `s`, the closure of `s` in `R` equals `s`.
|
NonUnitalSubsemiring.subset_closure
theorem NonUnitalSubsemiring.subset_closure :
∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {s : Set R}, s ⊆ ↑(NonUnitalSubsemiring.closure s)
This theorem states that for any type `R` with a non-unital, non-associative semiring structure, and any set `s` of elements of `R`, the set `s` is included in (or is a subset of) the non-unital subsemiring generated by `s`. In other words, every element of `s` is also an element of the non-unital subsemiring generated by `s`.
More concisely: For any non-unital semiring `R` and set `s` of elements in `R`, `s` is contained in the non-unital subsemiring generated by `s`.
|
NonUnitalRingHom.srange_top_of_surjective
theorem NonUnitalRingHom.srange_top_of_surjective :
∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
{F : Type u_1} [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (f : F),
Function.Surjective ⇑f → NonUnitalRingHom.srange f = ⊤
This theorem states that if we have a non-unital ring homomorphism, represented by a function `f` from a type `R` to a type `S`, where both `R` and `S` are non-unital, non-associative semirings, then if this function `f` is surjective (meaning that every element in `S` is the image of some element in `R` under `f`), the range of this homomorphism becomes the entire codomain `S`. In other words, a surjective non-unital ring homomorphism maps to every element in the codomain.
More concisely: If `f` is a surjective non-unital ring homomorphism from a non-unital semiring `R` to a non-unital semiring `S`, then the image of `f` equals `S`.
|
NonUnitalSubsemiring.gc_map_comap
theorem NonUnitalSubsemiring.gc_map_comap :
∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
{F : Type u_1} [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (f : F),
GaloisConnection (NonUnitalSubsemiring.map f) (NonUnitalSubsemiring.comap f)
This theorem, `NonUnitalSubsemiring.gc_map_comap`, states that for any non-unital non-associative semirings `R` and `S`, and for any function `f` of type `F` that is a non-unital ring homomorphism from `R` to `S` and also satisfies the `FunLike` property (meaning it can be injectively coerced to a function from `R` to `S`), there exists a Galois connection between the function `NonUnitalSubsemiring.map f` and the function `NonUnitalSubsemiring.comap f`. In other words, for any elements `a` from the codomain and `b` from the domain, `NonUnitalSubsemiring.map f a ≤ b` if and only if `a ≤ NonUnitalSubsemiring.comap f b`. Here, `NonUnitalSubsemiring.map f` is a function that applies `f` to each element of a subsemiring of `R` and `NonUnitalSubsemiring.comap f` is a function that returns the preimage of a subsemiring of `S` under `f`.
More concisely: For any non-unital non-associative semirings R and S, and for any non-unital ring homomorphism f from R to S satisfying the FunLike property, there exists a Galois connection between the maps sending a subsemiring of R to its image under f and a subsemiring of S to its preimage under f.
|
NonUnitalRingHom.coe_srange
theorem NonUnitalRingHom.coe_srange :
∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
{F : Type u_1} [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (f : F),
↑(NonUnitalRingHom.srange f) = Set.range ⇑f
The theorem `NonUnitalRingHom.coe_srange` states that for any non-unital, non-associative semiring `R` and `S`, and any function `f` of type `F` that is a homomorphism between the semirings (`F` is `FunLike` from `R` to `S` and also a `NonUnitalRingHomClass`), the range of the homomorphism `f` when viewed as a subsemiring of `S` (`NonUnitalRingHom.srange f`) is equivalent to the set of all values that `f` can produce (the range of `f` in the ordinary sense, `Set.range ⇑f`). This result connects the algebraic structure (the non-unital subsemiring generated by the image of `f`) with the simpler set-theoretic concept of the range of a function.
More concisely: The range of a non-unital homomorphism between two non-associative semirings, viewed as a subsemiring in the target semiring, is equal to the image of the homomorphism.
|
Subsemigroup.nonUnitalSubsemiringClosure_eq_closure
theorem Subsemigroup.nonUnitalSubsemiringClosure_eq_closure :
∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (M : Subsemigroup R),
M.nonUnitalSubsemiringClosure = NonUnitalSubsemiring.closure ↑M
The theorem `Subsemigroup.nonUnitalSubsemiringClosure_eq_closure` states that for any type `R` that forms a `NonUnitalNonAssocSemiring` (a non-associative and non-unital semiring), and for any `Subsemigroup` `M` of `R`, the `NonUnitalSubsemiring` generated by `M` is precisely the same as the `NonUnitalSubsemiring.closure` of the set underlying `M`. In other words, the `NonUnitalSubsemiring` that we can generate by taking the closure of `M` (the smallest `NonUnitalSubsemiring` of `R` that contains `M`) is the same as the `NonUnitalSubsemiring` we get directly from `M` itself.
More concisely: For any non-unital, non-associative semiring `R` and its subsemigroup `M`, the non-unital subsemiring generated by `M` equals the closure of `M` in the non-unital subsemiring structure.
|
Set.mem_center_iff_addMonoidHom
theorem Set.mem_center_iff_addMonoidHom :
∀ (R : Type u) [inst : NonUnitalNonAssocSemiring R] (a : R),
a ∈ Set.center R ↔
AddMonoidHom.mulLeft a = AddMonoidHom.mulRight a ∧
AddMonoidHom.mul.compr₂ (AddMonoidHom.mulLeft a) = AddMonoidHom.mul.comp (AddMonoidHom.mulLeft a) ∧
AddMonoidHom.mul.comp (AddMonoidHom.mulRight a) = AddMonoidHom.mul.compl₂ (AddMonoidHom.mulLeft a) ∧
AddMonoidHom.mul.compr₂ (AddMonoidHom.mulRight a) = AddMonoidHom.mul.compl₂ (AddMonoidHom.mulRight a)
The theorem `Set.mem_center_iff_addMonoidHom` provides a point-free way to prove the membership of an element `a` in the center of a non-associative ring `R`. Specifically, it states that `a` belongs to the center of `R` if and only if the left multiplication by `a` is equal to the right multiplication by `a`, and certain conditions involving composition of `AddMonoidHom.mulLeft` and `AddMonoidHom.mulRight` with `AddMonoidHom.mul` are satisfied. These conditions can be particularly useful when working with types that have extensionality lemmas for the `R →+ R` function type.
More concisely: A non-associative ring element `a` is in the center if and only if left and right multiplication by `a` agree and certain compositions of multiplication homomorphisms satisfy equality.
|
Mathlib.RingTheory.NonUnitalSubsemiring.Basic._auxLemma.6
theorem Mathlib.RingTheory.NonUnitalSubsemiring.Basic._auxLemma.6 :
∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (x : R), (x ∈ ⊤) = True
This theorem, which is part of the Ring Theory in Mathlib and relates to Non-Unital Subsemiring, states that for any type `R` that is a `NonUnitalNonAssocSemiring`, any element `x` of `R` is an element of the top (`⊤`) element, which represents the whole set in this context. This is always true, regardless of the specific `x` or `R`. In mathematical terms, this means if `R` is a non-unital, non-associative semiring, then any `x` in `R` is also in the universal set.
More concisely: In any non-unital, non-associative semiring `R`, every element `x` belongs to the universal set `⊤`.
|
NonUnitalRingHom.map_sclosure
theorem NonUnitalRingHom.map_sclosure :
∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
{F : Type u_1} [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (f : F) (s : Set R),
NonUnitalSubsemiring.map f (NonUnitalSubsemiring.closure s) = NonUnitalSubsemiring.closure (⇑f '' s)
The theorem `NonUnitalRingHom.map_sclosure` states that for any non-unital, non-associative semiring `R` and `S`, if there is a ring homomorphism `f` from `R` to `S`, the image of the subsemiring generated by a set `s` of `R` under the homomorphism is equal to the subsemiring of `S` generated by the image of the set `s` under the homomorphism. This means that mapping a generating set through a ring homomorphism and then taking the subsemiring closure produces the same result as first taking the subsemiring closure and then mapping through the ring homomorphism.
More concisely: For any non-unital semirings R and S with a ring homomorphism f, the image of the subsemiring generated by a set s in R under f is equal to the subsemiring generated by the image of s in S.
|
NonUnitalSubsemiring.closure_induction
theorem NonUnitalSubsemiring.closure_induction :
∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {s : Set R} {p : R → Prop} {x : R},
x ∈ NonUnitalSubsemiring.closure s →
(∀ x ∈ s, p x) → p 0 → (∀ (x y : R), p x → p y → p (x + y)) → (∀ (x y : R), p x → p y → p (x * y)) → p x
This theorem describes an induction principle for membership in the closure of a set within a NonUnitalNonAssocSemiring. The theorem states that given a type `R` that forms a NonUnitalNonAssocSemiring, a set `s` of elements of `R`, a predicate `p` over `R`, and an element `x` of `R`, if `x` is in the closure of `s` and the predicate `p` holds for `0`, `1`, and all elements of `s`, and is also preserved under addition and multiplication (meaning that if `p` holds for two elements `x` and `y`, then `p` will also hold for `x + y` and `x * y`), then `p` will hold for `x`. This principle enables reasoning about all elements within the closure of `s` based on the properties of `s` and the operations of the semiring.
More concisely: If `s` is a set of elements in a NonUnitalNonAssocSemiring `R`, `p` is a predicate on `R` holding for `0`, `1`, and all elements in `s`, and `x` is in the closure of `s`, then `p(x)` holds if `p` is preserved under addition and multiplication.
|
NonUnitalSubsemiring.coe_closure_eq
theorem NonUnitalSubsemiring.coe_closure_eq :
∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (s : Set R),
↑(NonUnitalSubsemiring.closure s) = ↑(AddSubmonoid.closure ↑(Subsemigroup.closure s))
This theorem states that for any set `s` in a non-unital, non-associative semiring `R`, the elements of the non-unital subsemiring generated by `s` are precisely the same as the elements of the additive closure of the multiplicative subsemigroup generated by `s`. In simpler terms, it's saying that in a certain kind of algebraic structure (a non-unital, non-associative semiring), a certain type of closure (non-unital subsemiring) of a set is equal to the closure of another kind (additive closure of a multiplicative subsemigroup) of the same set.
More concisely: In a non-unital, non-associative semiring, the non-unital subsemiring generated by a set is equal to the additive closure of the multiplicative subsemigroup generated by that set.
|
NonUnitalSubsemiring.mul_mem'
theorem NonUnitalSubsemiring.mul_mem' :
∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (self : NonUnitalSubsemiring R) {a b : R},
a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
This theorem states that in the context of a non-unital, non-associative semiring `R`, for any subsemiring `self`, if two elements `a` and `b` are members of the carrier set of that subsemiring, then their product `a * b` is also a member of the same subsemiring's carrier set. This captures one of the key properties of a subsemigroup: closure under multiplication.
More concisely: In a non-unital, non-associative semiring `R`, the product of any two elements from a subsemiring's carrier set lies in the same subsemiring's carrier set.
|