isSubmonoid_iUnion_of_directed
theorem isSubmonoid_iUnion_of_directed :
∀ {M : Type u_1} [inst : Monoid M] {ι : Type u_3} [hι : Nonempty ι] {s : ι → Set M},
(∀ (i : ι), IsSubmonoid (s i)) → (∀ (i j : ι), ∃ k, s i ⊆ s k ∧ s j ⊆ s k) → IsSubmonoid (⋃ i, s i)
This theorem states that given a monoid `M`, and an indexed, directed, and nonempty set of submonoids of `M`, the union of these submonoids is also a submonoid of `M`. Here, the set of submonoids is indexed by a type `ι` (which is nonempty), and each element of `ι` maps to a submonoid of `M` (captured by the function `s : ι → Set M`). The directionality condition states that for any two indices `i` and `j`, there exists an index `k` such that the submonoids at indices `i` and `j` are both subsets of the submonoid at index `k`. The theorem then concludes that the union of all these submonoids (expressed as `(⋃ i, s i)`) is itself a submonoid of `M`.
More concisely: Given a monoid `M` and an indexed, directed, and nonempty family `(Si : ι → Set M)` of submonoids, the union `⋃ i, Si i` is also a submonoid of `M`.
|
IsSubmonoid.mul_mem
theorem IsSubmonoid.mul_mem :
∀ {M : Type u_1} [inst : Monoid M] {s : Set M}, IsSubmonoid s → ∀ {a b : M}, a ∈ s → b ∈ s → a * b ∈ s
This theorem, `IsSubmonoid.mul_mem`, states that for any type `M` equipped with a Monoid structure, and any set `s` of elements of type `M` which is a submonoid (according to the `IsSubmonoid` predicate), if elements `a` and `b` are members of `s`, then their product `a * b` is also a member of `s`. Essentially, this theorem asserts that the set `s` is closed under the multiplication operation of the Monoid.
More concisely: For any Monoid `M` and submonoid `s` of `M`, if `a, b ∈ s`, then `a * b ∈ s`.
|
IsAddSubmonoid.add_mem
theorem IsAddSubmonoid.add_mem :
∀ {A : Type u_2} [inst : AddMonoid A] {s : Set A}, IsAddSubmonoid s → ∀ {a b : A}, a ∈ s → b ∈ s → a + b ∈ s := by
sorry
This theorem states that for any type `A` that has an addition operation and is a monoid, if a set `s` of elements of type `A` is an additive submonoid, then for any two elements `a` and `b` of `A`, if both `a` and `b` are in `s`, their sum `a + b` is also in `s`. In other words, the set `s` is closed under the operation of addition.
More concisely: If `s` is an additive submonoid of a monoid `(A, +)` with operation `+`, then for all `a, b ∈ s`, `a + b ∈ s`.
|
IsSubmonoid.pow_mem
theorem IsSubmonoid.pow_mem :
∀ {M : Type u_1} [inst : Monoid M] {s : Set M} {a : M}, IsSubmonoid s → a ∈ s → ∀ {n : ℕ}, a ^ n ∈ s
This theorem states that submonoids are closed under natural powers. In other words, for any type `M` that forms a monoid, any set `s` of type `M` that is a submonoid, any element `a` of type `M`, and any natural number `n`, if `a` is an element of the submonoid `s`, then `a` raised to the power of `n` is also an element of the submonoid `s`.
More concisely: If `s` is a submonoid of the monoid `M`, then for all `a in s` and natural number `n`, `a^n` is also in `s`.
|
Monoid.closure_subset
theorem Monoid.closure_subset :
∀ {M : Type u_1} [inst : Monoid M] {s t : Set M}, IsSubmonoid t → s ⊆ t → Monoid.Closure s ⊆ t
This theorem states that for any type `M` that forms a Monoid, given two sets of elements `s` and `t` from `M`, if `t` is a submonoid and the set `s` is contained within `t`, then the submonoid generated by `s` (as defined by `Monoid.Closure`) is also contained within `t`. Essentially, this theorem shows that a submonoid generated by a subset of a larger submonoid remains within the bounds of the larger submonoid.
More concisely: If `s` is a subset of the submonoid `t` of a monoid `M`, then the submonoid generated by `s` (Monoid.Closure `s`) is contained within `t`.
|
Monoid.image_closure
theorem Monoid.image_closure :
∀ {M : Type u_1} [inst : Monoid M] {A : Type u_3} [inst_1 : Monoid A] {f : M → A},
IsMonoidHom f → ∀ (s : Set M), f '' Monoid.Closure s = Monoid.Closure (f '' s)
The theorem `Monoid.image_closure` states that for a given monoid `M`, another monoid `A`, a function `f` from `M` to `A` that respects the monoid structure (i.e., it's a monoid homomorphism), and a set `s` of elements from `M`, the image under the function `f` of the submonoid generated by the set `s` is the same as the submonoid generated by the image of the set `s` under the function `f`. In other words, applying a monoid homomorphism to the elements of a submonoid (generated by a set) creates the same result as generating a submonoid from the image of the original set under the homomorphism.
More concisely: Let `M` be a monoid, `A` another monoid, `f : M → A` a monoid homomorphism, and `s ⊆ M` a set. Then, the submonoid of `A` generated by `f''s` is equal to `f''(msub M s)`, where `msub M s` denotes the submonoid of `M` generated by `s`.
|
IsSubmonoid.inter
theorem IsSubmonoid.inter :
∀ {M : Type u_1} [inst : Monoid M] {s₁ s₂ : Set M}, IsSubmonoid s₁ → IsSubmonoid s₂ → IsSubmonoid (s₁ ∩ s₂) := by
sorry
The theorem `IsSubmonoid.inter` states that for any type `M` that has a Monoid structure, and any two subsets `s₁` and `s₂` of `M` that are submonoids, their intersection (denoted `s₁ ∩ s₂`) is also a submonoid of `M`. A submonoid is a subset that itself forms a monoid with the inherited operation, and the intersection of two sets is the set of elements that belong to both sets.
More concisely: If `M` is a monoid and `s₁` and `s₂` are its subsets that are submonoids, then their intersection `s₁ ∩ s₂` is also a submonoid of `M`.
|
IsAddSubmonoid.preimage
theorem IsAddSubmonoid.preimage :
∀ {M : Type u_1} [inst : AddMonoid M] {N : Type u_3} [inst_1 : AddMonoid N] {f : M → N},
IsAddMonoidHom f → ∀ {s : Set N}, IsAddSubmonoid s → IsAddSubmonoid (f ⁻¹' s)
This theorem states that for any types `M` and `N` which are both `AddMonoid`s (i.e., have addition operation that is associative and has an identity element 0), if `f` is an `AddMonoid` homomorphism from `M` to `N` (i.e., a function preserving the addition operation and the identity element), and `s` is an `AddSubmonoid` of `N` (i.e., a subset of `N` that is also an `AddMonoid`), then the preimage of `s` under `f` (the set of all elements in `M` that map to elements of `s` under `f`) is also an `AddSubmonoid` of `M`.
More concisely: If `f` is an additive homomorphism from an additive monoid `M` to an additive monoid `N` and `s` is an additive submonoid of `N`, then the preimage of `s` under `f` is an additive submonoid of `M`.
|
Range.isAddSubmonoid
theorem Range.isAddSubmonoid :
∀ {M : Type u_1} [inst : AddMonoid M] {γ : Type u_3} [inst_1 : AddMonoid γ] {f : M → γ},
IsAddMonoidHom f → IsAddSubmonoid (Set.range f)
This theorem states that for any function `f` from type `M` to type `γ`, if `M` and `γ` are both Additive Monoids and `f` is a homomorphism of Additive Monoids, then the range of `f` (the set of all its possible output values) forms an Additive Submonoid of `γ`. In other words, if `f` respects the operation of addition and `0` from `M` to `γ`, its image under `f` will also respect the operation of addition and contain the additive identity in `γ`.
More concisely: If `f` is a homomorphism of additive monoids from an additive monoid `M` to an additive monoid `γ`, then the range of `f` is an additive submonoid of `γ`.
|
AddMonoid.mem_closure_union_iff
theorem AddMonoid.mem_closure_union_iff :
∀ {M : Type u_3} [inst : AddCommMonoid M] {s t : Set M} {x : M},
x ∈ AddMonoid.Closure (s ∪ t) ↔ ∃ y ∈ AddMonoid.Closure s, ∃ z ∈ AddMonoid.Closure t, y + z = x
This theorem, titled `AddMonoid.mem_closure_union_iff`, states that for any type `M` assuming a commutative `AddMonoid` structure and given two sets `s` and `t` of this type, any element `x` in `M` belongs to the additively generated submonoid of `M` by the union of `s` and `t` if and only if there exists an element 'y' in the additively generated submonoid by `s` and an element 'z' in the additively generated submonoid by `t` such that 'y' plus 'z' equals `x`. In other words, any element in the additive closure of the union of two sets can be expressed as the sum of an element from the additive closure of each set.
More concisely: For any commutative add monoid M and sets s, t of M, an element x belongs to the additively generated submonoid of M by the union of s and t if and only if there exist y in the additive closure of s and z in the additive closure of t such that x = y + z.
|
IsSubmonoid.one_mem
theorem IsSubmonoid.one_mem : ∀ {M : Type u_1} [inst : Monoid M] {s : Set M}, IsSubmonoid s → 1 ∈ s
The theorem `IsSubmonoid.one_mem` states that for any given type `M` which has a Monoid instance, and for any set `s` of type `M`, if `s` is a submonoid, then the identity element `1` is a member of `s`. In other words, it asserts that the identity element is always included in the set that forms a submonoid in the context of monoid theory.
More concisely: If `M` is a monoid and `s` is a submonoid of `M`, then `1 ∈ s`.
|
IsAddSubmonoid.multiples_subset
theorem IsAddSubmonoid.multiples_subset :
∀ {M : Type u_1} [inst : AddMonoid M] {s : Set M} {a : M}, IsAddSubmonoid s → a ∈ s → multiples a ⊆ s
The theorem `IsAddSubmonoid.multiples_subset` states that for any type `M` which is an Additive Monoid, for any set `s` of type `M` and for any element `a` of `M`, if `s` is an Additive Submonoid and `a` is an element of `s`, then the set of natural number multiples of `a` is a subset of `s`. In other words, if we have a submonoid and pick an element from it, all natural number multiples of this element will also be elements of this submonoid.
More concisely: For any Additive Monoid M, if S is an Additive Submonoid of M containing an element a, then the set {n \* a | n : ℕ} is a subset of S.
|
IsSubmonoid.image
theorem IsSubmonoid.image :
∀ {M : Type u_1} [inst : Monoid M] {γ : Type u_3} [inst_1 : Monoid γ] {f : M → γ},
IsMonoidHom f → ∀ {s : Set M}, IsSubmonoid s → IsSubmonoid (f '' s)
The theorem `IsSubmonoid.image` states that for any given types `M` and `γ`, where `M` and `γ` are monoids, and for any function `f` from `M` to `γ` which is a monoid homomorphism, for any subset `s` of `M` that is a submonoid, the image of `s` under `f` is a submonoid of `γ`. In simpler terms, the image of a submonoid under a monoid homomorphism is also a submonoid.
More concisely: If `f` is a monoid homomorphism from monoid `M` to monoid `γ`, and `s` is a submonoid of `M`, then `f(s)` is a submonoid of `γ`.
|
IsAddSubmonoid.nsmul_mem
theorem IsAddSubmonoid.nsmul_mem :
∀ {M : Type u_1} [inst : AddMonoid M] {s : Set M} {a : M}, IsAddSubmonoid s → a ∈ s → ∀ {n : ℕ}, n • a ∈ s := by
sorry
The theorem `IsAddSubmonoid.nsmul_mem` states that for any given type `M` that has an `AddMonoid` structure, if a set `s` of `M` is an `AddSubmonoid`, then any element `a` of this set `s` when multiplied by any natural number `n` (using the notation `n • a` for natural number multiplication) remains in the set `s`. In other words, an `AddSubmonoid` is closed under multiplication by natural numbers.
More concisely: If `M` is an AddMonoid and `s` is an AddSubmonoid of `M`, then for all `a ∈ s` and `n ∈ ℕ`, we have `n • a ∈ s`.
|
Monoid.subset_closure
theorem Monoid.subset_closure : ∀ {M : Type u_1} [inst : Monoid M] {s : Set M}, s ⊆ Monoid.Closure s
This theorem states that for any given monoid `M` and a subset `s` of this monoid, the subset `s` is contained within the submonoid generated by `s` itself. In other words, every element in the subset `s` also belongs to the submonoid created by taking the closure of `s` under the monoid operations. This property holds true for all monoids and their subsets.
More concisely: For any monoid M and subset s of M, s is contained in the submonoid generated by s.
|
Univ.isSubmonoid
theorem Univ.isSubmonoid : ∀ {M : Type u_1} [inst : Monoid M], IsSubmonoid Set.univ
This theorem states that for any type `M` that has a `Monoid` structure, the universal set of `M` is a submonoid of `M` itself. In other words, every monoid is considered a submonoid of itself, given the universal set contains all elements of the type - in this case, all elements of the monoid `M`.
More concisely: For any type `M` equipped with a monoid structure, the universal set of `M` is a submonoid of `M`.
|
IsAddSubmonoid.multiset_sum_mem
theorem IsAddSubmonoid.multiset_sum_mem :
∀ {M : Type u_3} [inst : AddCommMonoid M] {s : Set M},
IsAddSubmonoid s → ∀ (m : Multiset M), (∀ a ∈ m, a ∈ s) → m.sum ∈ s
This theorem states that given a type `M` that forms an additive commutative monoid, a set `s` of elements of `M` that forms an additive submonoid, and a multiset `m` of elements of `M`, if every element of `m` belongs to `s`, then the sum of all elements in `m` also belongs to the set `s`. Essentially, it shows that the sum of a collection of elements from an additive submonoid stays within the submonoid.
More concisely: Given an additive commutative monoid `M`, an additive submonoid `s` of `M`, and a multiset `m` of elements from `s`, the sum of all elements in `m` belongs to `s`.
|
Monoid.mem_closure_union_iff
theorem Monoid.mem_closure_union_iff :
∀ {M : Type u_3} [inst : CommMonoid M] {s t : Set M} {x : M},
x ∈ Monoid.Closure (s ∪ t) ↔ ∃ y ∈ Monoid.Closure s, ∃ z ∈ Monoid.Closure t, y * z = x
This theorem states that for any commutative monoid, denoted by `M`, and given any two sets `s` and `t` of `M`, and an element `x` of `M`, `x` is an element of the submonoid generated by the union of `s` and `t` if and only if there exists an element `y` in the submonoid generated by `s` and an element `z` in the submonoid generated by `t` such that the product of `y` and `z` equals `x`. In other words, an element is in the submonoid generated by the union of two sets if and only if it can be expressed as the product of an element from the submonoid generated by each set.
More concisely: An element of a commutative monoid belongs to the submonoid generated by two sets if and only if it can be expressed as the product of elements from each set.
|
Monoid.closure_singleton
theorem Monoid.closure_singleton : ∀ {M : Type u_1} [inst : Monoid M] {x : M}, Monoid.Closure {x} = powers x
This theorem states that for any monoid `M` and any element `x` of `M`, the submonoid generated by the singleton set `{x}` is equal to the set of natural number powers of `x`. In other words, if we take a monoid (which is a set equipped with an associative binary operation and an identity element), and an element `x` from that monoid, the set that includes `x` and all results of applying the monoid operation to `x` and itself an arbitrary number of times (also known as the submonoid generated by `x`), is exactly the same set as the set of all natural number powers of `x` (i.e., `{1, x, x², x³, ...}`).
More concisely: For any monoid `M` and element `x` in `M`, the submonoid generated by `{x}` equals the set of natural number powers of `x`.
|
IsSubmonoid.power_subset
theorem IsSubmonoid.power_subset :
∀ {M : Type u_1} [inst : Monoid M] {s : Set M} {a : M}, IsSubmonoid s → a ∈ s → powers a ⊆ s
The theorem `IsSubmonoid.power_subset` states that for any type `M` that is a monoid and any set `s` of elements of `M` that is a submonoid, if an element `a` of `M` is in `s`, then the set of natural number powers of `a`, i.e., the set `{1, a, a², ...}`, is a subset of `s`. In other words, all natural number powers of any element in a submonoid also belong to the same submonoid.
More concisely: If `M` is a monoid and `s` is a submonoid of `M` containing an element `a`, then the set {`a^n | n : ℕ`} ⊆ `s`.
|
IsAddSubmonoid.zero_mem
theorem IsAddSubmonoid.zero_mem : ∀ {A : Type u_2} [inst : AddMonoid A] {s : Set A}, IsAddSubmonoid s → 0 ∈ s := by
sorry
This theorem, named `IsAddSubmonoid.zero_mem`, states that for any type `A` that is an additive monoid, and any set `s` of elements of this type, if `s` is an additive submonoid, then the additive identity element `0` is a member of `s`. In mathematical terms, if we have an additive monoid `(A, +, 0)` and `s` is a subset of `A` such that `s` is a submonoid under the operation `+`, then `0` belongs to `s`.
More concisely: If `(A, +, 0)` is an additive monoid and `s ⊆ A` is an additive submonoid, then `0 ∈ s`.
|
IsSubmonoid.iInter
theorem IsSubmonoid.iInter :
∀ {M : Type u_1} [inst : Monoid M] {ι : Sort u_3} {s : ι → Set M},
(∀ (y : ι), IsSubmonoid (s y)) → IsSubmonoid (Set.iInter s)
The theorem `IsSubmonoid.iInter` states that for any type `M` that has a `Monoid` instance and for any family `s` of sets, indexed by some type `ι`, if each set `s y` is a submonoid of `M` (for every `y` of type `ι`), then the intersection of all these sets, `Set.iInter s`, is also a submonoid of `M`. In mathematical terms, if every set `s(y)`, for `y` in `ι`, is a submonoid of a monoid `M`, then the intersection of all such `s(y)` forms a submonoid of `M`.
More concisely: If each `s y` is a submonoid of a monoid `M`, then the intersection `Set.iInter s` is also a submonoid of `M`.
|
powers.self_mem
theorem powers.self_mem : ∀ {M : Type u_1} [inst : Monoid M] {x : M}, x ∈ powers x
The theorem `powers.self_mem` states that, for any given element `x` of a monoid `M`, this element `x` is a member of its own set of natural number powers. In other words, for every element `x` in a monoid `M`, there exists a natural number `n` such that `x^n = x`. This is a basic property of exponents in a monoid, as raising any element to the power of 1 will yield the element itself.
More concisely: For every element x in a monoid, there exists a natural number n such that x^n = x. (A monoid element has the property that raising it to some power equals itself.)
|
powers.one_mem
theorem powers.one_mem : ∀ {M : Type u_1} [inst : Monoid M] {x : M}, 1 ∈ powers x
This theorem states that for any given monoid `M` and any element `x` of `M`, the element `1` is contained within the set of natural number powers of `x`. In other words, `1` can be expressed as `x` raised to some natural number `n` in the context of a monoid.
More concisely: For any monoid `M` and element `x` in `M`, there exists a natural number `n` such that `1 = x^n`.
|
Monoid.exists_list_of_mem_closure
theorem Monoid.exists_list_of_mem_closure :
∀ {M : Type u_1} [inst : Monoid M] {s : Set M} {a : M}, a ∈ Monoid.Closure s → ∃ l, (∀ x ∈ l, x ∈ s) ∧ l.prod = a
The theorem `Monoid.exists_list_of_mem_closure` states that for any monoid `M` and any subset `s` of `M`, if an element `a` belongs to the submonoid generated by `s` (denoted by `Monoid.Closure s`), then there exists a list of elements from `s` such that the product of all elements in the list equals `a`. In other words, any element in the submonoid generated by a set can be expressed as the product of a sequence of elements from the original set.
More concisely: For any monoid `M` and subset `s` of `M`, if an element `a` belongs to the submonoid generated by `s`, then there exists a finite list `[x₁, ..., xₙ]` of elements from `s` such that `a = ∏(x₁, ..., xₙ)`.
|
AddMonoid.closure_subset
theorem AddMonoid.closure_subset :
∀ {M : Type u_1} [inst : AddMonoid M] {s t : Set M}, IsAddSubmonoid t → s ⊆ t → AddMonoid.Closure s ⊆ t
The theorem `AddMonoid.closure_subset` states that for any type `M` equipped with an additive monoid structure, if we have two sets `s` and `t` of elements of `M`, such that `t` is an additive submonoid and `s` is a subset of `t`, then the additive submonoid generated by `s` (denoted as `AddMonoid.Closure s`) is also a subset of `t`. In other words, every additive submonoid that contains a certain set also contains the additive submonoid generated by that set.
More concisely: For any additive monoid `M` and subsets `s` of `t` of `M` with `t` being an additive submonoid, `AddMonoid.Closure s` (the additive submonoid generated by `s`) is a subset of `t`.
|
multiples.add_mem
theorem multiples.add_mem :
∀ {M : Type u_1} [inst : AddMonoid M] {x y z : M}, y ∈ multiples x → z ∈ multiples x → y + z ∈ multiples x := by
sorry
The theorem states that for any type `M` that is an instance of an `AddMonoid`, and for any elements `y`, `z`, and `x` of that type, if `y` and `z` are in the set of natural number multiples of `x`, then the addition of `y` and `z` will also be in the set of natural number multiples of `x`. In other words, the set of natural number multiples of an element in an additive monoid is closed under addition.
More concisely: If `M` is an add monoid type and `x, y, z : M` with `y` and `z` being natural number multiples of `x`, then `y + z` is also a natural number multiple of `x`.
|
AddMonoid.closure_singleton
theorem AddMonoid.closure_singleton :
∀ {M : Type u_1} [inst : AddMonoid M] {x : M}, AddMonoid.Closure {x} = multiples x
This theorem states that for any type `M` forming an additive monoid, and for any element `x` of this monoid, the additive submonoid generated by the singleton set containing `x` is equal to the set of natural number multiples of `x`. In other words, the smallest submonoid containing `x` consists exactly of the elements that can be obtained by adding `x` to itself a certain number of times.
More concisely: For any additive monoid `M` and element `x` in `M`, the submonoid generated by `x` equals the set of natural number multiples of `x`.
|
Univ.isAddSubmonoid
theorem Univ.isAddSubmonoid : ∀ {M : Type u_1} [inst : AddMonoid M], IsAddSubmonoid Set.univ
This theorem states that for any type `M`, given that `M` is an additive monoid (`AddMonoid`), the universal set of `M` (`Set.univ`) is an additive submonoid (`AddSubmonoid`). In other words, any additive monoid is also an additive submonoid of itself. This is a general property that holds for all additive monoids.
More concisely: For any additive monoid `M`, the universal set of `M` is an additive submonoid of `M`.
|
IsSubmonoid.preimage
theorem IsSubmonoid.preimage :
∀ {M : Type u_1} [inst : Monoid M] {N : Type u_3} [inst_1 : Monoid N] {f : M → N},
IsMonoidHom f → ∀ {s : Set N}, IsSubmonoid s → IsSubmonoid (f ⁻¹' s)
This theorem states that the preimage of a submonoid under a monoid homomorphism is itself a submonoid of the original monoid's domain. Specifically, given a monoid `M`, a monoid `N`, and a monoid homomorphism `f` from `M` to `N`, if `s` is a submonoid of `N`, then the preimage of `s` under `f` (denoted `f⁻¹'s`) is a submonoid of `M`. Here, a monoid is a set equipped with an associative binary operation and an identity element, a submonoid is a subset of a monoid that is itself a monoid, and a monoid homomorphism is a function between two monoids that preserves the monoid structure.
More concisely: Given a monoid homomorphism from a monoid M to a monoid N and a submonoid s of N, the preimage of s under f is a submonoid of M.
|
IsAddSubmonoid.inter
theorem IsAddSubmonoid.inter :
∀ {M : Type u_1} [inst : AddMonoid M] {s₁ s₂ : Set M},
IsAddSubmonoid s₁ → IsAddSubmonoid s₂ → IsAddSubmonoid (s₁ ∩ s₂)
The theorem `IsAddSubmonoid.inter` states that for any type `M` that is an `AddMonoid`, the intersection of two `AddSubmonoid`s of `M` is also an `AddSubmonoid` of `M`. In other words, if you have two subsets `s₁` and `s₂` of `M` that are both `AddSubmonoid`s, their intersection (the set of elements common to both `s₁` and `s₂`) is also an `AddSubmonoid`. This highlights a fundamental property of submonoids in the context of addition, showing how they can be combined through intersection while still preserving the `AddSubmonoid` structure.
More concisely: For any `AddMonoid` `M`, if `s₁` and `s₂` are two `AddSubmonoids` of `M`, then their intersection `s₁ ∩ s₂` is also an `AddSubmonoid` of `M`.
|
IsAddSubmonoid.list_sum_mem
theorem IsAddSubmonoid.list_sum_mem :
∀ {M : Type u_1} [inst : AddMonoid M] {s : Set M},
IsAddSubmonoid s → ∀ {l : List M}, (∀ x ∈ l, x ∈ s) → l.sum ∈ s
This theorem states that for any type `M` that has an `AddMonoid` structure, any `Set` of `M`, if that set is an additive submonoid, then for any list of elements of `M`, if every element of the list belongs to the set, the sum of the elements in the list also belongs to the set. In other words, the sum of a list of elements from an additive submonoid remains within the submonoid.
More concisely: For any additive submonoid `S` of an `AddMonoid` type `M`, the sum of any list of elements from `S` belongs to `S`.
|
multiples.isAddSubmonoid
theorem multiples.isAddSubmonoid : ∀ {M : Type u_1} [inst : AddMonoid M] (x : M), IsAddSubmonoid (multiples x) := by
sorry
This theorem states that for any element `x` in an `AddMonoid` `M`, the set of natural number multiples of `x` forms an `AddSubmonoid` of `M`. In other words, if you take any element in `M` and consider the set of its multiples using the natural numbers (i.e., `{0, x, 2x, ...}`), that set will also have the structure of an additive submonoid.
More concisely: For any `AddMonoid M` and its element `x`, the set of natural number multiples of `x` is an additive submonoid of `M`.
|
AddMonoid.closure_mono
theorem AddMonoid.closure_mono :
∀ {M : Type u_1} [inst : AddMonoid M] {s t : Set M}, s ⊆ t → AddMonoid.Closure s ⊆ AddMonoid.Closure t
The theorem `AddMonoid.closure_mono` states that for any type `M` that forms an `AddMonoid` and any two subsets `s` and `t` of `M`, if `s` is a subset of `t`, then the additive submonoid generated by `s` is a subset of the additive submonoid generated by `t`. In other words, if we generate submonoids by repeatedly adding elements from `s` or `t`, any element that can be made by adding elements from `s` can also be made by adding elements from `t`, provided `s` is a subset of `t`.
More concisely: For any additive monoid M and subsets s, t of M with s subseteq t, the additive submonoid generated by s is contained in the additive submonoid generated by t.
|
multiples.self_mem
theorem multiples.self_mem : ∀ {M : Type u_1} [inst : AddMonoid M] {x : M}, x ∈ multiples x
The theorem `multiples.self_mem` states that for any element `x` in an additive monoid `M`, `x` is a member of the set of its own natural number multiples. In other words, `x` is in the set that includes `0, x, 2x, ...`. This makes sense as `x` is a multiple of itself, given that every element in an additive monoid can be expressed as the sum of one or more copies of itself.
More concisely: For every additive monoid element x, x belongs to the set of its natural number multiples.
|
IsSubmonoid.finset_prod_mem
theorem IsSubmonoid.finset_prod_mem :
∀ {M : Type u_3} {A : Type u_4} [inst : CommMonoid M] {s : Set M},
IsSubmonoid s → ∀ (f : A → M) (t : Finset A), (∀ b ∈ t, f b ∈ s) → (t.prod fun b => f b) ∈ s
This theorem states that for any commutative monoid `M` and any set `s` of elements from `M` that forms a submonoid, if we have a function `f` mapping from some type `A` to `M`, and a finite set `t` of elements of type `A`, then if every element `b` in `t` when mapped by `f` is an element of the submonoid `s`, the product of these mapped elements (or equivalently, the product of `f b` for all `b` in `t`) is also an element of the submonoid `s`. This means that the submonoid is closed under the operation of taking the product of a finite number of its elements (via a function from a finite set), which is a fundamental property of a submonoid in a commutative monoid.
More concisely: Given a commutative monoid `M`, a submonoid `s`, a function `f : A -> M`, and a finite set `t` of `A` such that `f(b)` is in `s` for all `b` in `t`, then the product of `f(b)` for all `b` in `t` is in `s`.
|
IsAddSubmonoid.finset_sum_mem
theorem IsAddSubmonoid.finset_sum_mem :
∀ {M : Type u_3} {A : Type u_4} [inst : AddCommMonoid M] {s : Set M},
IsAddSubmonoid s → ∀ (f : A → M) (t : Finset A), (∀ b ∈ t, f b ∈ s) → (t.sum fun b => f b) ∈ s
The theorem `IsAddSubmonoid.finset_sum_mem` states that for any types `M` and `A`, if `M` is an additive commutative monoid and `s` is a subset of `M` that forms an additive submonoid, then for any function `f` from `A` to `M` and any finite set `t` of elements of `A`, if every element of `t` when mapped by `f` is in `s`, the sum of the elements of `t` under the function `f` will also be in the submonoid `s`. In simpler terms, if you have a set of elements, and summing any combination of them stays within the set, then the set is an additive submonoid.
More concisely: If `s` is an additive submonoid of an additive commutative monoid `M`, and for every finite set `t` of elements in some type `A` such that `f(a) ∈ s` for all `a ∈ t`, then `∑ a ∈ t f(a) ∈ s`.
|
Monoid.closure.isSubmonoid
theorem Monoid.closure.isSubmonoid : ∀ {M : Type u_1} [inst : Monoid M] (s : Set M), IsSubmonoid (Monoid.Closure s)
This theorem states that for any type `M` which is a monoid, and any set `s` of elements of `M`, the monoid closure of `s` (denoted by `Monoid.Closure s`) forms a submonoid of `M`. In other words, the set of elements that can be obtained by repeatedly applying the monoid operation to the elements of `s` (and their results) is itself a monoid.
More concisely: For any monoid `M` and set `s` of its elements, `Monoid.Closure s` is a submonoid of `M`.
|
IsAddSubmonoid.iInter
theorem IsAddSubmonoid.iInter :
∀ {M : Type u_1} [inst : AddMonoid M] {ι : Sort u_3} {s : ι → Set M},
(∀ (y : ι), IsAddSubmonoid (s y)) → IsAddSubmonoid (Set.iInter s)
The theorem `IsAddSubmonoid.iInter` states that for any type `M` that has an `AddMonoid` structure, an index set `ι`, and a function `s` mapping from `ι` to a set of elements in `M`, if every set `s y` for `y` in `ι` forms an additive submonoid, then the intersection of all these sets also forms an additive submonoid. Here, an additive submonoid is a subset of `M` that contains the additive identity, is closed under addition, and is closed under taking additive inverses. The intersection of a collection of sets is the set of elements shared by all the sets in that collection.
More concisely: Given a type `M` with an `AddMonoid` structure, an index set `ι`, and a function `s : ι → M` such that for all `y in ι`, `s y` is an additive submonoid, the intersection of all `s y` forms an additive submonoid of `M`.
|
AddMonoid.image_closure
theorem AddMonoid.image_closure :
∀ {M : Type u_1} [inst : AddMonoid M] {A : Type u_3} [inst_1 : AddMonoid A] {f : M → A},
IsAddMonoidHom f → ∀ (s : Set M), f '' AddMonoid.Closure s = AddMonoid.Closure (f '' s)
This theorem states that for any two types `M` and `A` that are both instances of an `AddMonoid`, and for any function `f` from type `M` to `A` that is an `AddMonoid` homomorphism, the image of the `AddSubmonoid` generated by a certain set `s` under the function `f` is equal to the `AddSubmonoid` generated by the image of the set `s` under the same function `f`. In mathematical terms, if $M$ and $A$ are additive monoids and $f: M \to A$ is a homomorphism, then the image of the closure of a subset of $M$ under $f$ is equal to the closure of the image of the subset under $f$.
More concisely: For any additive monoids M and A and additive monoid homomorphism f from M to A, the image of the subadditive submonoid generated by a subset of M under f is equal to the subadditive submonoid generated by the image of that subset under f.
|
AddMonoid.closure.isAddSubmonoid
theorem AddMonoid.closure.isAddSubmonoid :
∀ {M : Type u_1} [inst : AddMonoid M] (s : Set M), IsAddSubmonoid (AddMonoid.Closure s)
This theorem states that for any given type `M` that forms an `AddMonoid`, and for any set `s` of elements of type `M`, the closure of `s` under the operation of the `AddMonoid` forms an `AddSubmonoid`. In other words, if you start with a set of elements in an additive monoid and include all the elements that can be obtained by adding elements from that set, the resulting set is guaranteed to be an additive submonoid of the original monoid.
More concisely: Given an additive monoid `M` and a subset `s` of `M`, the closure of `s` under the `AddMonoid` operation forms an additive submonoid.
|
IsSubmonoid.multiset_prod_mem
theorem IsSubmonoid.multiset_prod_mem :
∀ {M : Type u_3} [inst : CommMonoid M] {s : Set M},
IsSubmonoid s → ∀ (m : Multiset M), (∀ a ∈ m, a ∈ s) → m.prod ∈ s
The theorem `IsSubmonoid.multiset_prod_mem` states that for any commutative monoid `M`, any subset `s` of `M` that forms a submonoid, and any multiset `m` of elements from `M`, if every element of `m` belongs to `s`, then the product of all elements in `m` (denoted by `m.prod`) also belongs to the submonoid `s`. In other words, the product of a multiset of elements from a submonoid of a commutative monoid is itself an element of that submonoid. This is a property that arises from the closure condition in the definition of a submonoid, namely that the product of any elements in a submonoid is also in the submonoid.
More concisely: Given a commutative monoid M and a submonoid s of M, if every element in the multiset m belongs to s, then the product of all elements in m belongs to s.
|
AddMonoid.exists_list_of_mem_closure
theorem AddMonoid.exists_list_of_mem_closure :
∀ {M : Type u_1} [inst : AddMonoid M] {s : Set M} {a : M},
a ∈ AddMonoid.Closure s → ∃ l, (∀ x ∈ l, x ∈ s) ∧ l.sum = a
This theorem states that, for any given type `M` equipped with an addition operation (i.e., an `AddMonoid M`), and any subset `s` of `M`, if an element `a` belongs to the additive submonoid generated by `s` (i.e., `a` is in `AddMonoid.Closure s`), then we can find a list of elements `l` from the set `s` such that the sum of all elements in `l` is exactly `a`. Furthermore, each element `x` in the list `l` must be from the set `s`.
In other words, any element in the closure of a set under addition can be expressed as the sum of a list of elements from the original set.
More concisely: For any additive monoid `(M, +)` and subset `s` of `M`, every element `a` in the additive submonoid generated by `s` can be expressed as the sum of a finite list of elements from `s`.
|
multiples.zero_mem
theorem multiples.zero_mem : ∀ {M : Type u_1} [inst : AddMonoid M] {x : M}, 0 ∈ multiples x
The theorem `multiples.zero_mem` states that for any given type `M` that has an `AddMonoid` structure, and any element `x` of `M`, the number 0 is included in the set of natural number multiples of `x`. In other words, the additive identity (0) is always a multiple of any element in an additive monoid.
More concisely: For any AddMonoid type M and its element x, 0 is a multiple of x.
|
powers.mul_mem
theorem powers.mul_mem :
∀ {M : Type u_1} [inst : Monoid M] {x y z : M}, y ∈ powers x → z ∈ powers x → y * z ∈ powers x
The theorem states that for any type `M` with a monoid structure, for any elements `y` and `z` of `M` that belong to the set of natural number powers of another element `x` of `M`, their product `y * z` also belongs to the set of natural number powers of `x`. In other words, the set of natural number powers of an element in a monoid is closed under multiplication.
More concisely: In a monoid, the set of natural number powers of an element is closed under multiplication.
|
IsAddSubmonoid.image
theorem IsAddSubmonoid.image :
∀ {M : Type u_1} [inst : AddMonoid M] {γ : Type u_3} [inst_1 : AddMonoid γ] {f : M → γ},
IsAddMonoidHom f → ∀ {s : Set M}, IsAddSubmonoid s → IsAddSubmonoid (f '' s)
This theorem states that for any given types `M` and `γ` where both are `AddMonoid`s, and for any function `f` from `M` to `γ` that is an `AddMonoid` homomorphism, if `s` is an `AddSubmonoid` of `M`, then the image of `s` under `f` (denoted as `f '' s`) is an `AddSubmonoid` of `γ`. In simpler terms, if `s` is a subset of `M` that forms an additive submonoid and `f` is a function that preserves the additive monoid structure, the image (or the result of applying `f` to each element of `s`) will also be an additive submonoid in the codomain `γ`.
More concisely: Given types `M` and `γ` that are AddMonoids, and a homomorphism `f` from `M` to `γ`, if `s` is an AddSubmonoid of `M`, then `f '' s` is an AddSubmonoid of `γ`.
|
AddMonoid.subset_closure
theorem AddMonoid.subset_closure : ∀ {M : Type u_1} [inst : AddMonoid M] {s : Set M}, s ⊆ AddMonoid.Closure s := by
sorry
This theorem states that for any given set `s` which is a subset of an additive monoid `M`, the set `s` is a subset (or is contained within) the additive submonoid generated by `s` itself. In other words, every element of `s` is also an element of the additive submonoid that `s` generates. This is a fundamental property in the study of monoids and their subsets.
More concisely: For any subset `s` of an additive monoid `M`, `s` is contained in the additive submonoid generated by `s`.
|
Range.isSubmonoid
theorem Range.isSubmonoid :
∀ {M : Type u_1} [inst : Monoid M] {γ : Type u_3} [inst_1 : Monoid γ] {f : M → γ},
IsMonoidHom f → IsSubmonoid (Set.range f)
The theorem `Range.isSubmonoid` states that for any given types `M` and `γ` that are both monoids, and any function `f` from `M` to `γ` that is a monoid homomorphism, the range (the set of all possible outputs) of the function `f` is a submonoid of the codomain `γ`. In simpler words, the image set of a monoid homomorphism is always a submonoid of the target monoid.
More concisely: The image of a monoid homomorphism between monoids is a submonoid.
|
IsSubmonoid.list_prod_mem
theorem IsSubmonoid.list_prod_mem :
∀ {M : Type u_1} [inst : Monoid M] {s : Set M}, IsSubmonoid s → ∀ {l : List M}, (∀ x ∈ l, x ∈ s) → l.prod ∈ s := by
sorry
The theorem `IsSubmonoid.list_prod_mem` states that for any type `M` that is a monoid and any set `s` of elements of `M` that is a submonoid, if every element of a given list `l` of elements of `M` is in `s`, then the product of all elements in `l` is also in `s`. In other words, the product of a list of elements of a submonoid remains in the submonoid.
More concisely: If `M` is a monoid and `s` is a submonoid of `M`, then for any list `l` of elements in `s`, the product of elements in `l` belongs to `s`.
|
Monoid.closure_mono
theorem Monoid.closure_mono :
∀ {M : Type u_1} [inst : Monoid M] {s t : Set M}, s ⊆ t → Monoid.Closure s ⊆ Monoid.Closure t
This theorem states that for any given subsets `s` and `t` of a monoid `M`, if `s` is a subset of `t` then the submonoid generated by `s` is also a subset of the submonoid generated by `t`. In mathematical terms, this can be expressed as: if $s \subseteq t$, then the closure of $s$ under the monoid operation (which forms a submonoid of `M`) is contained within the closure of `t` under the same operation. This captures the intuitive idea that adding more elements to generate a submonoid can't result in a smaller submonoid.
More concisely: If `s` is a subset of `t` in a monoid `M`, then the submonoid generated by `s` is contained in the submonoid generated by `t`.
|
powers.isSubmonoid
theorem powers.isSubmonoid : ∀ {M : Type u_1} [inst : Monoid M] (x : M), IsSubmonoid (powers x)
This theorem states that for any given monoid `M` and any element `x` of `M`, the set of natural number powers of `x` forms a submonoid of `M`. In other words, when you take any element from a monoid and construct a set with this element raised to all natural number powers, this set will always satisfy the properties of a submonoid within the original monoid.
More concisely: For any monoid M and its element x, the set {x^n | n is a natural number} is a submonoid of M.
|
isAddSubmonoid_iUnion_of_directed
theorem isAddSubmonoid_iUnion_of_directed :
∀ {M : Type u_1} [inst : AddMonoid M] {ι : Type u_3} [hι : Nonempty ι] {s : ι → Set M},
(∀ (i : ι), IsAddSubmonoid (s i)) → (∀ (i j : ι), ∃ k, s i ⊆ s k ∧ s j ⊆ s k) → IsAddSubmonoid (⋃ i, s i)
This theorem states that the union of an indexed, directed, nonempty set of additive submonoids of an additive monoid `M` is also an additive submonoid of `M`. In other words, given a type `M` with an additive monoid structure, a nonempty indexing type `ι`, and a family of sets `s : ι → Set M` such that each `s i` is an additive submonoid, if for any two indices `i` and `j` there exists an index `k` such that both `s i` and `s j` are subsets of `s k` (i.e., the family of sets is directed), then the union of all these sets (⋃ i, s i) forms an additive submonoid of `M`.
More concisely: Given an additive monoid `M`, a nonempty indexed family `(s : ι → Sets M)` of additive submonoids with the property that for any pair of indices `i, j`, there exists an index `k` such that `s i ⊆ s k` and `s j ⊆ s k`, the union `⋃ i, s i` is an additive submonoid of `M`.
|