AddSubsemigroup.not_mem_bot
theorem AddSubsemigroup.not_mem_bot : ∀ {M : Type u_1} [inst : Add M] {x : M}, x ∉ ⊥
This theorem states that for any type `M` that supports addition operation (denoted by `[inst : Add M]`), no element `x` from `M` belongs to the bottom element (denoted by `⊥`). In simple terms, it's stating that no element of an additive semigroup can be the bottom element.
More concisely: There exists no element in an additive semigroup that satisfies the property of being the additive identity and the bottom element at the same time.
|
Subsemigroup.closure_induction₂
theorem Subsemigroup.closure_induction₂ :
∀ {M : Type u_1} [inst : Mul M] {s : Set M} {p : M → M → Prop} {x y : M},
x ∈ Subsemigroup.closure s →
y ∈ Subsemigroup.closure s →
(∀ x ∈ s, ∀ y ∈ s, p x y) →
(∀ (x y z : M), p x z → p y z → p (x * y) z) → (∀ (x y z : M), p z x → p z y → p z (x * y)) → p x y
This theorem, `Subsemigroup.closure_induction₂`, is an induction principle for membership in the closure of a set with respect to a subsemigroup. Given a type `M` equipped with a multiplication operation, a set `s` of elements of that type, and a predicate `p` that takes two elements of `M`, it states that for any two elements `x` and `y` that belong to the closure of `s` under the subsemigroup operations, if the predicate `p` holds for all pairs of elements in `s`, and if it is preserved under multiplication in both arguments, then `p` must hold for `x` and `y`. The preservation under multiplication is stated by saying that if `p` holds for `x, z` and `y, z`, then it holds for `(x * y), z`, and similarly, if `p` holds for `z, x` and `z, y`, then it holds for `z, (x * y)`.
More concisely: If `s` is a set closed under a subsemigroup operation on type `M`, `p(x, y)` holds for all `x, y ∈ s`, and `p` is preserving under multiplication in both arguments, then `p(x, y)` holds for all `x, y` in the closure of `s`.
|
AddSubsemigroup.closure_induction'
theorem AddSubsemigroup.closure_induction' :
∀ {M : Type u_1} [inst : Add M] (s : Set M) {p : (x : M) → x ∈ AddSubsemigroup.closure s → Prop},
(∀ (x : M) (h : x ∈ s), p x ⋯) →
(∀ (x : M) (hx : x ∈ AddSubsemigroup.closure s) (y : M) (hy : y ∈ AddSubsemigroup.closure s),
p x hx → p y hy → p (x + y) ⋯) →
∀ {x : M} (hx : x ∈ AddSubsemigroup.closure s), p x hx
The theorem `AddSubsemigroup.closure_induction'` is a dependent version of `AddSubsemigroup.closure_induction`. It states that for any type `M` with an addition operation and a set `s` of elements of this type, given a property `p` that is dependent on an element `x` of type `M` and the fact that `x` belongs to the additive subsemigroup generated by `s`, if `p` holds for all elements in `s` and if `p` is preserved under the addition operation for any two elements in the additive subsemigroup generated by `s`, then `p` holds for all elements in the additive subsemigroup generated by `s`.
More concisely: If `s` is an additive subsemigroup of a type `M` with addition, and `p(x)` is a property dependent on `x` and its membership in `s`, such that `p` holds for all elements in `s` and is closed under addition of elements in `s`, then `p` holds for all elements in the additive subsemigroup generated by `s`.
|
AddSubsemigroup.add_mem
theorem AddSubsemigroup.add_mem :
∀ {M : Type u_1} [inst : Add M] (S : AddSubsemigroup M) {x y : M}, x ∈ S → y ∈ S → x + y ∈ S
This theorem states that for any type `M` that is equipped with an addition operation, any `AddSubsemigroup` of `M`, and any two elements `x` and `y` of `M`, if both `x` and `y` are elements of the `AddSubsemigroup`, then their sum `x + y` is also an element of the `AddSubsemigroup`. In other words, an `AddSubsemigroup` is closed under the operation of addition.
More concisely: Given an additive semigroup (AddSubsemigroup) `S` in a type `M` with addition operation, for all `x, y ∈ S`, their sum `x + y` also belongs to `S`.
|
AddSubsemigroup.closure_induction₂
theorem AddSubsemigroup.closure_induction₂ :
∀ {M : Type u_1} [inst : Add M] {s : Set M} {p : M → M → Prop} {x y : M},
x ∈ AddSubsemigroup.closure s →
y ∈ AddSubsemigroup.closure s →
(∀ x ∈ s, ∀ y ∈ s, p x y) →
(∀ (x y z : M), p x z → p y z → p (x + y) z) → (∀ (x y z : M), p z x → p z y → p z (x + y)) → p x y
This theorem is an induction principle for membership in the additive closure of a set. Given a type `M` with an addition operation, a set `s` of elements of `M`, and a predicate `p` that takes two elements of `M`, if `x` and `y` are members of the additive closure of `s`, and the predicate `p` holds for all pairs of elements of `s`, then for any three elements `x`, `y`, and `z` of `M`, if `p` holds for the pairs `(x, z)` and `(y, z)`, and if `p` also holds for the pairs `(z, x)` and `(z, y)`, then `p` must hold for the pair `(x, y)`. This principle can be used to prove properties about elements in the additive closure of a set based on properties of elements in the original set and their sums.
More concisely: If a set `s` of elements in an additive group `M` satisfies the property `p` for all pairs of elements in `s`, and `x`, `y`, and `z` are in the additive closure of `s` with `p(x, z)`, `p(y, z)`, `p(z, x)`, and `p(z, y)`, then `p(x, y)` holds.
|
Subsemigroup.closure_induction'
theorem Subsemigroup.closure_induction' :
∀ {M : Type u_1} [inst : Mul M] (s : Set M) {p : (x : M) → x ∈ Subsemigroup.closure s → Prop},
(∀ (x : M) (h : x ∈ s), p x ⋯) →
(∀ (x : M) (hx : x ∈ Subsemigroup.closure s) (y : M) (hy : y ∈ Subsemigroup.closure s),
p x hx → p y hy → p (x * y) ⋯) →
∀ {x : M} (hx : x ∈ Subsemigroup.closure s), p x hx
The theorem `Subsemigroup.closure_induction'` establishes an induction principle for the closure of a given set `s` in a multiplicative structure `M`. Specifically, we are given a property `p` that takes an element `x` of `M` and a proof that `x` is in the closure of `s` and returns a Proposition. This theorem states that if `p` holds for every element in `s` and for any two elements `x` and `y` in the closure of `s`, if `p` holds for `x` and `y` then it also holds for the product `x * y`, then `p` must hold for every element in the closure of `s`. This provides a way to prove a property over all elements in the closure of a set in a subsemigroup, given that the property holds for elements in the set and is preserved under the multiplication operation.
More concisely: If a property that holds for every element in a set `s` and is preserved under multiplication also holds for the product of any two elements in the closure of `s`, then the property holds for every element in the closure of `s`.
|
Mathlib.GroupTheory.Subsemigroup.Basic._auxLemma.7
theorem Mathlib.GroupTheory.Subsemigroup.Basic._auxLemma.7 : ∀ {M : Type u_1} [inst : Mul M] (x : M), (x ∈ ⊤) = True
This theorem, `Mathlib.GroupTheory.Subsemigroup.Basic._auxLemma.7`, states that for any type `M` equipped with a multiplication operation (i.e., `M` is a semigroup), any element `x` of type `M` is an element of the top element of the order of subsemigroups. In mathematical terms, it means that for any element `x` in a semigroup `M`, `x` belongs to the universal subsemigroup, denoted by `⊤`.
More concisely: Every element in a semigroup belongs to its universal subsemigroup.
|
AddSubsemigroup.closure_mono
theorem AddSubsemigroup.closure_mono :
∀ {M : Type u_1} [inst : Add M] ⦃s t : Set M⦄, s ⊆ t → AddSubsemigroup.closure s ≤ AddSubsemigroup.closure t := by
sorry
The theorem `AddSubsemigroup.closure_mono` states that the additive subsemigroup closure operation is monotonic with respect to set inclusion. In other words, for any type `M` with an addition operation and any two sets `s` and `t` of type `M`, if `s` is a subset of `t`, then the additive subsemigroup generated by `s` is a subsemigroup of the additive subsemigroup generated by `t`.
More concisely: For any additive subsemigroup `S` of a type `M` with addition, if `s` is a subset of `t` in `M`, then the additive subsemigroup generated by `s` is contained in the additive subsemigroup generated by `t`.
|
AddSubsemigroup.subset_closure
theorem AddSubsemigroup.subset_closure :
∀ {M : Type u_1} [inst : Add M] {s : Set M}, s ⊆ ↑(AddSubsemigroup.closure s)
The theorem, `AddSubsemigroup.subset_closure`, asserts that for any set `s` of a type `M` equipped with an addition operation, the set `s` is a subset of the additive subsemigroup generated by `s`. In other words, every element of the original set `s` is also an element of the additive subsemigroup formed by the closure operation on `s`.
More concisely: For any set `s` and type `M` with an addition operation, `s` is a subset of the additive subsemigroup generated by `s`.
|
AddSubsemigroup.add_mem'
theorem AddSubsemigroup.add_mem' :
∀ {M : Type u_4} [inst : Add M] (self : AddSubsemigroup M) {a b : M},
a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
This theorem states that for any type `M` with an addition operation, if you have an additive subsemigroup of `M` and two elements `a` and `b` that belong to this subsemigroup, then their sum `a + b` also belongs to the subsemigroup. This property is fundamental to the definition of a subsemigroup in mathematics.
More concisely: Given a type `M` with an addition operation and a subsemigroup `S`, if `a, b ∈ S`, then `a + b ∈ S`.
|
Subsemigroup.closure_mono
theorem Subsemigroup.closure_mono :
∀ {M : Type u_1} [inst : Mul M] ⦃s t : Set M⦄, s ⊆ t → Subsemigroup.closure s ≤ Subsemigroup.closure t
This theorem states that the subsemigroup closure of a set is monotone with respect to set inclusion. In other words, if we have two sets `s` and `t` of a certain type `M` (where `M` is equipped with a multiplication operation), and if `s` is a subset of `t` (`s ⊆ t`), then the subsemigroup generated by `s` is a subsemigroup of or equal to the subsemigroup generated by `t`. This is denoted as `Subsemigroup.closure s ≤ Subsemigroup.closure t`.
More concisely: If `s` is a subset of `t` in a semigroup, then the subsemigroup generated by `s` is contained in or equal to the subsemigroup generated by `t`.
|
Subsemigroup.dense_induction
theorem Subsemigroup.dense_induction :
∀ {M : Type u_1} [inst : Mul M] {p : M → Prop} (x : M) {s : Set M},
Subsemigroup.closure s = ⊤ → (∀ x ∈ s, p x) → (∀ (x y : M), p x → p y → p (x * y)) → p x
This theorem is called `Subsemigroup.dense_induction` and it provides a way to prove a property holds for all elements of a magma `M` using a dense induction method. If a set `s` is dense in `M` such that the closure of `s` under the subsemigroup operation equals the whole set `M` (i.e., `Subsemigroup.closure s = ⊤`), the theorem states that to prove a predicate `p` holds for all `x : M ` it's sufficient to verify two conditions: (1) the predicate `p` holds for all elements `x` in `s`, and (2) given any two elements `x` and `y` of `M` for which `p` holds, `p` also holds for their product `x * y`.
More concisely: If a dense set `s` of a magma `M` satisfies `Subsemigroup.closure s = M`, then to prove a property `p(x)` holds for all `x` in `M`, it's sufficient to verify `p(s)` holds for all elements in `s` and `p(x)` holds for any two elements `x` and `y` with `p(x)` and `p(y)`.
|
AddSubsemigroup.ext
theorem AddSubsemigroup.ext :
∀ {M : Type u_1} [inst : Add M] {S T : AddSubsemigroup M}, (∀ (x : M), x ∈ S ↔ x ∈ T) → S = T
This theorem states that for any given type `M` that has an addition operation, if there are two AddSubsemigroups `S` and `T` of type `M` such that any element `x` of type `M` that is in `S` is also in `T` and vice versa, then the two AddSubsemigroups `S` and `T` are equal. An AddSubsemigroup is simply a subset of elements that still form a semigroup under the addition operation, so this theorem is essentially saying that if two subsets contain exactly the same elements, they are the same subset.
More concisely: If `S` and `T` are AddSubsemigroups of type `M` with the property that every element in `S` is also in `T` and vice versa, then `S` is equal to `T`.
|
Subsemigroup.mul_mem
theorem Subsemigroup.mul_mem :
∀ {M : Type u_1} [inst : Mul M] (S : Subsemigroup M) {x y : M}, x ∈ S → y ∈ S → x * y ∈ S
This theorem states that for any type `M` which has a multiplication operation defined, and for any subsemigroup `S` of `M`, if elements `x` and `y` are members of `S`, then the product of `x` and `y` (`x * y`) is also a member of `S`. In essence, this theorem proves that a subsemigroup is closed under multiplication, which is a fundamental property of semigroups.
More concisely: If `S` is a subsemigroup of a type `M` with multiplication, then `x * y` belongs to `S` for all `x, y` in `S`.
|
AddHom.eqOn_closure
theorem AddHom.eqOn_closure :
∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f g : AddHom M N} {s : Set M},
Set.EqOn (⇑f) (⇑g) s → Set.EqOn ⇑f ⇑g ↑(AddSubsemigroup.closure s)
This theorem states that if two additive homomorphisms (functions that preserve the addition operation) are equal on a set, then they are also equal on the closure of that set under the operation of forming additive subsemigroups. In other words, if for all elements in the set, the two functions map an element to the same value, then this property will still hold when we extend the set to its additive subsemigroup closure. Here, the additive subsemigroup closure of a set is the smallest additive subsemigroup that contains the set.
More concisely: If two additive homomorphisms agree on a set, then they agree on its additive subsemigroup closure.
|
AddSubsemigroup.dense_induction
theorem AddSubsemigroup.dense_induction :
∀ {M : Type u_1} [inst : Add M] {p : M → Prop} (x : M) {s : Set M},
AddSubsemigroup.closure s = ⊤ → (∀ x ∈ s, p x) → (∀ (x y : M), p x → p y → p (x + y)) → p x
This theorem, `AddSubsemigroup.dense_induction`, states that if we have a set `s` which is dense in an additive monoid `M`, denoted by `AddSubsemigroup.closure s = ⊤`, and we want to prove that some predicate `p` holds for all elements `x` of `M`. In this scenario, it is enough to confirm that `p x` is true for every element `x` in the set `s`, and that for any two elements `x` and `y` in `M`, if `p x` and `p y` hold true, then `p (x + y)` must also be true. Thus, the theorem provides a strategy for proving properties about all elements of an additive monoid based on the properties of a dense subset and the additive structure.
More concisely: If a dense subset `s` of an additive monoid `M` satisfies `p x` for all `x` in `s` and `p x + p y => p (x + y)`, then `p` holds for all elements of `M`.
|
Subsemigroup.ext
theorem Subsemigroup.ext : ∀ {M : Type u_1} [inst : Mul M] {S T : Subsemigroup M}, (∀ (x : M), x ∈ S ↔ x ∈ T) → S = T
This theorem states that two subsemigroups of a multiplicative type `M` are equal if and only if they have the same elements. In other words, for any type `M` equipped with a multiplication operation, if for every element `x` of `M` the condition of `x` being in subsemigroup `S` is equivalent to `x` being in subsemigroup `T`, then `S` and `T` must be the same subsemigroup.
More concisely: Two subsemigroups of a multiplicative type equal if and only if they have the same elements.
|
AddSubsemigroup.closure_le
theorem AddSubsemigroup.closure_le :
∀ {M : Type u_1} [inst : Add M] {s : Set M} {S : AddSubsemigroup M}, AddSubsemigroup.closure s ≤ S ↔ s ⊆ ↑S := by
sorry
This theorem states that for any type `M` that has an additive structure, a set `s` of elements of type `M`, and an additive subsemigroup `S` of `M`, the closure of `s` under the operation of `AddSubsemigroup` is included in `S` if and only if `s` is a subset of `S`. In other words, an additive subsemigroup `S` contains the least additive subsemigroup generated by a set `s` (the "closure" of `s`) if and only if `S` contains every element of `s`.
More concisely: An additive subsemigroup contains the closure of a subset if and only if the subset is a subset of the subsemigroup.
|
AddSubsemigroup.closure_eq
theorem AddSubsemigroup.closure_eq :
∀ {M : Type u_1} [inst : Add M] (S : AddSubsemigroup M), AddSubsemigroup.closure ↑S = S
The theorem `AddSubsemigroup.closure_eq` states that for any type `M` that has an addition structure, and for any additive subsemigroup `S` of `M`, the additive closure of `S` is equal to `S` itself. In other words, the closure operation, when applied to an additive subsemigroup, does not add any new elements to the subsemigroup.
More concisely: For any additive subsemigroup `S` of a type `M` with addition, the additive closure of `S` equals `S`.
|
Subsemigroup.closure_induction
theorem Subsemigroup.closure_induction :
∀ {M : Type u_1} [inst : Mul M] {s : Set M} {p : M → Prop} {x : M},
x ∈ Subsemigroup.closure s → (∀ x ∈ s, p x) → (∀ (x y : M), p x → p y → p (x * y)) → p x
The theorem `Subsemigroup.closure_induction` is an induction principle for membership in the closure of a set in a semigroup. It states that for any type `M` with a multiplication operation, a set `s` of elements of `M`, a property `p` that elements of `M` might satisfy, and an element `x` of `M`, if `x` is in the closure of `s` under the semigroup operation, and if `p` is true for all elements of `s` and is preserved under the multiplication operation (i.e., whenever `p` is true for two elements `x` and `y`, it is also true for their product `x * y`), then `p` is true for `x`. This essentially allows us to prove properties about elements in the closure of `s` by showing they hold for elements in `s` and are preserved under multiplication.
More concisely: If `s` is a closed semigroup under multiplication, `x` is in the closure of `s`, and `p(y)` holds for all `y` in `s` with `p(x * y)` following from `p(x)` and `p(y)`, then `p(x)` holds.
|
Subsemigroup.mem_closure
theorem Subsemigroup.mem_closure :
∀ {M : Type u_1} [inst : Mul M] {s : Set M} {x : M},
x ∈ Subsemigroup.closure s ↔ ∀ (S : Subsemigroup M), s ⊆ ↑S → x ∈ S
This theorem states that for any type `M` with multiplication, any set `s` of elements of this type, and any element `x` of this type, `x` is in the subsemigroup generated by `s` if and only if for any subsemigroup `S` containing the set `s`, `x` is also in `S`. In other words, an element is in the closure of a set in a multiplication structure if it belongs to every subsemigroup that contains the set.
More concisely: An element is in the closure of a set in a multiplicative structure if and only if it belongs to every subsemigroup containing the set.
|
AddMemClass.add_mem
theorem AddMemClass.add_mem :
∀ {S : Type u_4} {M : Type u_5} [inst : Add M] [inst_1 : SetLike S M] [self : AddMemClass S M] {s : S} {a b : M},
a ∈ s → b ∈ s → a + b ∈ s
This theorem states that for any type `S` and `M` where `M` has an addition operation, `S` behaves like a set of elements of type `M`, and `S` satisfies the `AddMemClass` property, then for any `s` of type `S` and any `a` and `b` of type `M`, if `a` and `b` are elements of `s`, then their sum `a + b` is also an element of `s`. In other words, a substructure that fulfills the `AddMemClass` property is closed under the addition operation.
More concisely: If `S` is a substructure of `M` with the `AddMemClass` property, then for all `s ∈ S` and `a, b ∈ M`, if `a, b ∈ s`, then `a + b ∈ s`.
|
Subsemigroup.closure_eq
theorem Subsemigroup.closure_eq : ∀ {M : Type u_1} [inst : Mul M] (S : Subsemigroup M), Subsemigroup.closure ↑S = S
The theorem `Subsemigroup.closure_eq` states that for any type `M` that has a multiplication operation and for any subsemigroup `S` of `M`, the closure of `S` is equal to `S` itself. Here, the closure of a set in a semigroup is the smallest subsemigroup that contains it. This means that applying the closure operation to a set that is already a subsemigroup does not modify the set.
More concisely: For any subsemigroup `S` of a type `M` with multiplication operation, `S` is equal to its closure in `M`.
|
Subsemigroup.closure_le
theorem Subsemigroup.closure_le :
∀ {M : Type u_1} [inst : Mul M] {s : Set M} {S : Subsemigroup M}, Subsemigroup.closure s ≤ S ↔ s ⊆ ↑S
The theorem `Subsemigroup.closure_le` states that for any type `M` with a multiplication operation and for any set `s` of elements in `M` and any subsemigroup `S` of `M`, the subsemigroup generated by the closure of `s` is a subset of `S` if and only if the set `s` itself is a subset of `S`. This theorem encapsulates an important property of subsemigroups in relation to the concept of closure, showing that the inclusion of the closure of a set in a subsemigroup implies the inclusion of the set itself, and vice versa.
More concisely: The subsemigroup generated by the closure of a set is contained in the subsemigroup if and only if the original set is contained in it.
|
AddSubsemigroup.closure_induction
theorem AddSubsemigroup.closure_induction :
∀ {M : Type u_1} [inst : Add M] {s : Set M} {p : M → Prop} {x : M},
x ∈ AddSubsemigroup.closure s → (∀ x ∈ s, p x) → (∀ (x y : M), p x → p y → p (x + y)) → p x
This theorem, named `AddSubsemigroup.closure_induction`, establishes an induction principle for membership in the closure of an additive subsemigroup. Given a type `M` with an addition operation, a set `s` of elements of `M`, a property `p` that elements of `M` might have, and an element `x` of `M`, the theorem states that: if `x` is in the closure of the additive subsemigroup generated by `s`, if `p` holds for all elements in `s`, and if `p` is preserved under the addition operation (that is, if you know `p` holds for `x` and `y`, then you can conclude that `p` holds for `x + y`), then `p` must also hold for `x`.
More concisely: If `s` is an additive subsemigroup of a type `M` with closure `C`, `p` is a property preserved under addition, and every element in `s` has property `p`, then any element `x` in the closure `C` also has property `p`.
|
Mathlib.GroupTheory.Subsemigroup.Basic._auxLemma.8
theorem Mathlib.GroupTheory.Subsemigroup.Basic._auxLemma.8 : ∀ {M : Type u_1} [inst : Add M] (x : M), (x ∈ ⊤) = True
This theorem states that for any type `M` equipped with addition operation (making it an additive semigroup), any element `x` of `M` always belongs to the 'top' or the universal set (`⊤`). In essence, it asserts that all elements of an additive semigroup are members of the universal set.
More concisely: Every element of an additive semigroup belongs to its universe.
|
Subsemigroup.subset_closure
theorem Subsemigroup.subset_closure : ∀ {M : Type u_1} [inst : Mul M] {s : Set M}, s ⊆ ↑(Subsemigroup.closure s) := by
sorry
This theorem states that for any type `M` equipped with a multiplication operation (making it a semigroup), and any subset `s` of `M`, the subsemigroup generated by `s` always includes `s`. In other words, every element of the set `s` also belongs to the subsemigroup generated by `s`. This is expressed formally by saying that `s` is a subset of the closure of `s` under the semigroup operation, denoted `Subsemigroup.closure s`.
More concisely: For any semigroup (M, \*), and subset s of M, s is a subset of the subsemigroup generated by s (denoted Subsemigroup.closure s).
|
Mathlib.GroupTheory.Subsemigroup.Basic._auxLemma.2
theorem Mathlib.GroupTheory.Subsemigroup.Basic._auxLemma.2 :
∀ {M : Type u_1} [inst : Add M] {s : AddSubsemigroup M} {x : M}, (x ∈ s.carrier) = (x ∈ s)
This theorem states that for any type `M` equipped with addition (notated as `Add M`), for any additive subsemigroup `s` of `M` and for any element `x` of `M`, the property of `x` being in the carrier of `s` is equivalent to `x` being in `s` itself. Here, a carrier refers to the set of all elements of the subsemigroup. In other words, this theorem proves that there's no difference between saying an element belongs to the carrier of a subsemigroup and saying it belongs to the subsemigroup directly, in the context of additive semigroups.
More concisely: For any additive subsemigroup `s` of a type `M` with addition, the carrier of `s` equals `s` itself.
|
Subsemigroup.mul_mem'
theorem Subsemigroup.mul_mem' :
∀ {M : Type u_4} [inst : Mul M] (self : Subsemigroup M) {a b : M},
a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
This theorem states that for any type `M` that has multiplication, given a subsemigroup of `M` and any two elements `a` and `b` of `M`, if `a` and `b` are members of the subsemigroup's underlying set (or "carrier"), then the product of `a` and `b`, denoted by `a * b`, is also a member of this subsemigroup's carrier. This is a basic property of subsemigroups in algebra, reflecting the closure under multiplication.
More concisely: If `M` is a type with multiplication and `S` is a subsemigroup of `M`, then for all `a, b ∈ S`, `a * b ∈ S`.
|
MulHom.eqOn_closure
theorem MulHom.eqOn_closure :
∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f g : M →ₙ* N} {s : Set M},
Set.EqOn (⇑f) (⇑g) s → Set.EqOn ⇑f ⇑g ↑(Subsemigroup.closure s)
This theorem states that for any two multiplication homomorphisms `f` and `g` from a type `M` to a type `N`, both equipped with a multiplication operation, if these two homomorphisms are equal on a set `s` of elements from `M` (i.e., they produce the same result when applied to any element of `s`), then they will also be equal on the subsemigroup closure of `s`. In other words, the two homomorphisms have the same effect not only on the elements of `s`, but also on the entire subsemigroup generated by `s`.
More concisely: If two multiplication homomorphisms from a semigroup to another semigroup agree on a set generating the subsemigroup closure, then they are equal.
|
MulMemClass.mul_mem
theorem MulMemClass.mul_mem :
∀ {S : Type u_4} {M : Type u_5} [inst : Mul M] [inst_1 : SetLike S M] [self : MulMemClass S M] {s : S} {a b : M},
a ∈ s → b ∈ s → a * b ∈ s
This theorem states that for any types `S` and `M`, given that `M` has a multiplication operation, `S` is a subset-like structure of `M` and a `MulMemClass` (meaning that multiplication of elements of `M` respects `S`), if elements `a` and `b` are in a specific instance `s` of `S`, then the product `a * b` is also in `s`. Essentially, this expresses that a substructure satisfying the `MulMemClass` property is closed under the multiplication operation.
More concisely: If `S` is a subset-like structure of a type `M` with multiplication and `S` is closed under multiplication (i.e., `M`'s multiplication respects `S`), then the product of any two elements in `S` lies in `S`.
|
Subsemigroup.not_mem_bot
theorem Subsemigroup.not_mem_bot : ∀ {M : Type u_1} [inst : Mul M] {x : M}, x ∉ ⊥
This theorem states that for any type `M` with a multiplication operation (denoted by `Mul M`), any element `x` of `M` is not a member of the bottom element (denoted by `⊥`). In other words, no element of a multiplicative subsemigroup is part of the smallest subsemigroup.
More concisely: For any type equipped with a multiplication operation, no element is in the bottom element of the multiplicative subsemigroup.
|