AddSubmonoid.mul_mem_mul
theorem AddSubmonoid.mul_mem_mul :
∀ {R : Type u_4} [inst : NonUnitalNonAssocSemiring R] {M N : AddSubmonoid R} {m n : R},
m ∈ M → n ∈ N → m * n ∈ M * N
This is a theorem about the multiplication operation in a non-unital, non-associative semiring. Specifically, it states that for any type `R` that forms a non-unital non-associative semiring, and any two additive submonoids `M` and `N` of `R`, if a number `m` is in `M` and a number `n` is in `N`, then the product `m * n` is in the set created by multiplying elements from `M` and `N`. In other words, the product of elements from the submonoids is also an element of the product of the submonoids.
More concisely: For any non-unital, non-associative semiring `R`, and additive submonoids `M` and `N` of `R`, the product of any element from `M` with any element from `N` is an element of the submonoid generated by the products of elements from `M` and `N`.
|
AddSubmonoid.closure_mul_closure
theorem AddSubmonoid.closure_mul_closure :
∀ {R : Type u_4} [inst : NonUnitalNonAssocSemiring R] (S T : Set R),
AddSubmonoid.closure S * AddSubmonoid.closure T = AddSubmonoid.closure (S * T)
The theorem `AddSubmonoid.closure_mul_closure` states that for any type `R` that forms a non-unital non-associative semiring, and for any two sets `S` and `T` of this type, the additive submonoid generated by the set `S` multiplied by the additive submonoid generated by the set `T` is exactly the same as the additive submonoid generated by the set obtained by multiplying `S` and `T`. Here multiplication of sets refers to the set of all products of an element from the first set and an element from the second set.
More concisely: For any non-unital non-associative semiring type `R` and sets `S` and `T` of `R`, the additive submonoids generated by `S` and `T` respectively, are equal to the additive submonoid generated by their product `S ∩ T := {x * y | x ∈ S, y ∈ T}`.
|
AddSubmonoid.one_eq_closure_one_set
theorem AddSubmonoid.one_eq_closure_one_set :
∀ {R : Type u_4} [inst : AddMonoidWithOne R], 1 = AddSubmonoid.closure 1
This theorem states that for any type `R` which has a structure of an additive monoid with a distinguished element `1`, the singleton set containing just `1` generates an `add_submonoid` whose closure is `1`. In more mathematical terms, the closure of the set `{1}` under the operations of the additive monoid with one is equal to `1`.
More concisely: For any additive monoid `R` with identity `1`, the singleton set `{1}` generates an additive submonoid whose closure is `1`.
|
AddSubmonoid.neg_le
theorem AddSubmonoid.neg_le : ∀ {G : Type u_2} [inst : AddGroup G] (S T : AddSubmonoid G), -S ≤ T ↔ S ≤ -T
This theorem states that for any given type `G` that has an addition group structure, and for any two additive submonoids `S` and `T` of `G`, the negation (taking additive inverses) of `S` is a subset of `T` if and only if `S` is a subset of the negation of `T`. In other words, it's saying that the inverse of `S` being contained in `T` and `S` being contained in the inverse of `T` are equivalent conditions.
More concisely: For any additive submonoids `S` and `T` of an additive group `G`, `-S` is a subset of `T` if and only if `S` is a subset of `-T`.
|
AddSubmonoid.mul_le
theorem AddSubmonoid.mul_le :
∀ {R : Type u_4} [inst : NonUnitalNonAssocSemiring R] {M N P : AddSubmonoid R},
M * N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m * n ∈ P
This theorem establishes a condition for the product of two additive submonoids to be a subset of a third submonoid, in the context of a non-unital and non-associative semiring. Specifically, for any type `R` that forms a non-unital non-associative semiring, and any three additive submonoids `M`, `N` and `P` of `R`, it states that `M * N` is a subset of `P` if and only if for every element `m` in `M` and every element `n` in `N`, the product `m * n` is an element of `P`.
More concisely: For any non-unital and non-associative semiring `R`, and additive submonoids `M`, `N`, and `P` of `R`, `M * N ⊆ P` if and only if for all `m ∈ M` and `n ∈ N`, `m * n ∈ P`.
|