Submonoid.powers_eq_closure
theorem Submonoid.powers_eq_closure :
∀ {M : Type u_1} [inst : Monoid M] (n : M), Submonoid.powers n = Submonoid.closure {n}
The theorem `Submonoid.powers_eq_closure` states that for any type `M` that forms a monoid, and for any element `n` of `M`, the submonoid generated by the powers of `n` is the same as the submonoid generated by the closure of the set containing `n` alone. Specifically, taking all the powers of `n` (i.e., `n` to the power of every possible integer) gives us the same submonoid as taking the smallest submonoid that contains `n`.
More concisely: For any monoid `M` and element `n` in `M`, the submonoid generated by the powers of `n` equals the submonoid generated by the closure of `{n}`.
|
Submonoid.iSup_induction
theorem Submonoid.iSup_induction :
∀ {M : Type u_1} [inst : MulOneClass M] {ι : Sort u_4} (S : ι → Submonoid M) {C : M → Prop} {x : M},
x ∈ ⨆ i, S i → (∀ (i : ι), ∀ x ∈ S i, C x) → C 1 → (∀ (x y : M), C x → C y → C (x * y)) → C x
This theorem, `Submonoid.iSup_induction`, establishes an induction principle for elements of the supremum of a collection `S` of submonoids in a given `MulOneClass` `M`. If a property `C` holds for the multiplicative identity `1` and for all elements of each submonoid `S i`, and if `C` is preserved under multiplication (i.e., if `C` holds for `x` and `y`, then it also holds for the product `x * y`), then `C` must hold for all elements of the supremum of the submonoids. This theorem is parameterized over a type `M` with a multiplication and identity operation, an index type `ι`, a function `S` from `ι` to submonoids of `M`, a predicate `C` on `M`, and an element `x` of `M`.
More concisely: If `1` and each element in every submonoid `S i` of a `MulOneClass` `M` satisfy a property `C`, and `C` is multiplicatively closed, then every element in the supremum of the submonoids also satisfies `C`.
|
AddSubmonoid.mem_closure_singleton
theorem AddSubmonoid.mem_closure_singleton :
∀ {A : Type u_2} [inst : AddMonoid A] {x y : A}, y ∈ AddSubmonoid.closure {x} ↔ ∃ n, n • x = y
This theorem states that for any Additive Monoid `A` and any two elements `x` and `y` of `A`, `y` belongs to the additive submonoid generated by `{x}` if and only if there exists a natural number `n` such that `n` times `x` equals `y`. In other words, the additive submonoid generated by a single element in an additive monoid is simply the set of all natural number multiples of that element.
More concisely: For any Additive Monoid A and its element x, the additive submonoid generated by {x} equals the set of all elements y in A that can be written as n x for some natural number n.
|
Submonoid.mem_powers
theorem Submonoid.mem_powers : ∀ {M : Type u_1} [inst : Monoid M] (n : M), n ∈ Submonoid.powers n
This theorem states that for any type `M` that has a monoid structure, and for any element `n` of this type `M`, `n` is an element of the submonoid generated by `n`. In mathematical terms, for any monoid `M` and any element `n` in `M`, `n` belongs to the least submonoid of `M` that contains the set of all powers of `n`.
More concisely: For any monoid `M` and its element `n`, `n` is an element of the submonoid generated by `n`. In other words, the submonoid generated by `{n}` is equal to the submonoid generated by `{n, n^n, n^2, ...}`.
|
list_sum_mem
theorem list_sum_mem :
∀ {M : Type u_1} {B : Type u_3} [inst : AddMonoid M] [inst_1 : SetLike B M] [inst_2 : AddSubmonoidClass B M] {S : B}
{l : List M}, (∀ x ∈ l, x ∈ S) → l.sum ∈ S
The theorem `list_sum_mem` states that for any type `M` that forms an additive monoid, and any type `B` that behaves like a set of elements of `M`, if `B` is a class of additive submonoids of `M` and `S` is an instance of `B`, then for any list `l` of elements of `M`, if all elements of `l` are in `S`, the sum of the list `l` is also in `S`. In other words, the sum of a list of elements in an additive submonoid remains within the additive submonoid.
More concisely: For any additive monoid `M` and set of additive submonoids `B` containing an additive submonoid `S`, if all elements of a list `l` belong to `S`, then the sum of `l` belongs to `S`.
|
MulMemClass.mul_mem_add_closure
theorem MulMemClass.mul_mem_add_closure :
∀ {M : Type u_1} {R : Type u_4} [inst : NonUnitalNonAssocSemiring R] [inst_1 : SetLike M R]
[inst_2 : MulMemClass M R] {S : M} {a b : R},
a ∈ AddSubmonoid.closure ↑S → b ∈ AddSubmonoid.closure ↑S → a * b ∈ AddSubmonoid.closure ↑S
This theorem states that for any types `M` and `R`, where `M` is a set-like structure over `R` and `R` is a non-unital, non-associative semiring, if `S` is a structure of type `M` and `a` and `b` are elements of `R`, then the product of two elements that are within the additive closure of `S` (as defined by `AddSubmonoid.closure`) is also within the additive closure of `S`. In simpler terms, if you have a set `S` in a semiring `R` and you generate an additive submonoid `S'` by taking the closure of `S`, then the product of any two elements of `S'` will also be an element of `S'`. This follows from the closure properties of submonoids in ring theory.
More concisely: Given a set-like structure `S` over a non-unital, non-associative semiring `R`, the additive closure of `S` is a submonoid of `R` and thus contains the product of any two of its elements.
|
MulMemClass.mul_left_mem_add_closure
theorem MulMemClass.mul_left_mem_add_closure :
∀ {M : Type u_1} {R : Type u_4} [inst : NonUnitalNonAssocSemiring R] [inst_1 : SetLike M R]
[inst_2 : MulMemClass M R] {S : M} {a b : R},
a ∈ S → b ∈ AddSubmonoid.closure ↑S → a * b ∈ AddSubmonoid.closure ↑S
The theorem `MulMemClass.mul_left_mem_add_closure` states that for any types `M` and `R`, given an instance of a non-unital, non-associative semiring `R`, an instance of `SetLike M R`, an instance of `MulMemClass M R`, a set `S` of type `M`, and elements `a` and `b` of type `R`, if `a` is an element of `S` and `b` is an element of the additive closure of the set `S` (which is a submonoid generated by set `S`), then the product `a * b` is also an element of the additive closure of `S`. In other words, the additive closure of a multiplicative submonoid is closed under multiplication by elements of the original set.
More concisely: If `S` is a multiplicative submonoid of a semiring `R` and `a` is in `S` while `b` is in the additive closure of `S`, then `a * b` is in the additive closure of `S`.
|
prod_mem
theorem prod_mem :
∀ {B : Type u_3} {S : B} {M : Type u_4} [inst : CommMonoid M] [inst_1 : SetLike B M] [inst_2 : SubmonoidClass B M]
{ι : Type u_5} {t : Finset ι} {f : ι → M}, (∀ c ∈ t, f c ∈ S) → (t.prod fun c => f c) ∈ S
The theorem `prod_mem` states that for any type `B`, element `S` of `B`, commutative monoid `M`, and any indexing type `ι`, if you have a finite set `t` (of type `Finset ι`) and a function `f` that maps elements of `ι` to `M`, then the product of the function `f` applied to the elements of the finite set `t` (denoted by `Finset.prod t fun c => f c`) is an element of `S`. This holds if and only if for each element `c` in the finite set `t`, `f c` is an element of `S`. This theorem basically says that the product of elements of a submonoid of a commutative monoid, indexed by a finite set, remains in the submonoid.
More concisely: If `t` is a finite set, `B` a type, `S` an element of `B`, `M` a commutative monoid, and `f : ι → M` a function, then `Finset.prod t fun c => f c ∈ S` if and only if `∀c ∈ t, f c ∈ S`.
|
Submonoid.multiset_prod_mem
theorem Submonoid.multiset_prod_mem :
∀ {M : Type u_4} [inst : CommMonoid M] (S : Submonoid M) (m : Multiset M), (∀ a ∈ m, a ∈ S) → m.prod ∈ S
This theorem states that for any commutative monoid `M` and a submonoid `S` of `M`, the product of elements in a multiset `m` of `M` is in the submonoid `S` given that every element `a` in the multiset `m` is also in `S`. In other words, the product of a set of elements, which are all part of a certain submonoid, will also be a part of the same submonoid. This holds true for multisets, which are essentially sets that can contain duplicate elements.
More concisely: For any commutative monoid M and submonoid S, the product of a multiset of elements from S is an element of S.
|
list_prod_mem
theorem list_prod_mem :
∀ {M : Type u_1} {B : Type u_3} [inst : Monoid M] [inst_1 : SetLike B M] [inst_2 : SubmonoidClass B M] {S : B}
{l : List M}, (∀ x ∈ l, x ∈ S) → l.prod ∈ S
This theorem states that given a type `M` with a monoid structure, a type `B`, and `S` as a subset of `B` which forms a submonoid of `M`, if we have a list `l` of elements of `M` and every element of `l` is in `S`, then the product of the elements of `l` (i.e., `List.prod l`) is also in `S`. In other words, the product of a list of elements in a submonoid stays within that submonoid.
More concisely: Given a monoid `M` with a submonoid `S`, if `l` is a list of elements in `S`, then the product of `l` is also an element of `S`.
|
Submonoid.list_prod_mem
theorem Submonoid.list_prod_mem :
∀ {M : Type u_1} [inst : Monoid M] (s : Submonoid M) {l : List M}, (∀ x ∈ l, x ∈ s) → l.prod ∈ s
This theorem states that for any type `M` which forms a monoid, and any submonoid `s` of `M`, the product of elements in a list `l` (with elements from `M`) is an element of `s` if each individual element of `l` is in `s`. In mathematical terms, if each element `x` in `l` is an element of the submonoid `s`, then the product of all elements in `l` will also be an element of `s`.
More concisely: If `M` is a monoid and `s` is a submonoid of `M`, then the product of any list of elements from `s` belongs to `s`.
|
multiset_sum_mem
theorem multiset_sum_mem :
∀ {B : Type u_3} {S : B} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : SetLike B M]
[inst_2 : AddSubmonoidClass B M] (m : Multiset M), (∀ a ∈ m, a ∈ S) → m.sum ∈ S
This theorem states that the sum of a multiset of elements from an additive submonoid of a commutative additive monoid is also in the additive submonoid. In other words, if `B` is a type, `S` is a value of type `B`, `M` is another type, and `M` has a structure of a commutative additive monoid, then for any multiset of elements from `M`, if all elements of this multiset belong to `S`, then the sum of the elements of the multiset also belongs to `S`. This maintains the closure property of the submonoid, which says that the sum of any elements in the submonoid remains in the submonoid.
More concisely: If `S` is an additive submonoid of a commutative additive monoid `M`, then the sum of any multiset of elements from `S` is also in `S`.
|
AddSubmonoid.sum_mem
theorem AddSubmonoid.sum_mem :
∀ {M : Type u_4} [inst : AddCommMonoid M] (S : AddSubmonoid M) {ι : Type u_5} {t : Finset ι} {f : ι → M},
(∀ c ∈ t, f c ∈ S) → (t.sum fun c => f c) ∈ S
This theorem states that the sum of elements in an `AddSubmonoid` of an `AddCommMonoid`, indexed by a `Finset`, is also a member of the `AddSubmonoid`. More specifically, given a type `M` that forms an additive commutative monoid, an `AddSubmonoid` `S` of `M`, a finite set `t` of type `ι`, and a function `f` mapping from `ι` to `M`, if every element of `t` mapped through `f` is in `S`, then the sum of these elements (obtained by applying `f` to each element of `t` and summing the results) is also in `S`.
More concisely: Given an additive commutative monoid `M` with an additive submonoid `S`, if `f : ι → M` maps each element of a finite set `t ⊆ ι` to an element in `S`, then the sum of the images of `t` under `f` is also in `S`.
|
Submonoid.mem_closure_pair
theorem Submonoid.mem_closure_pair :
∀ {A : Type u_4} [inst : CommMonoid A] (a b c : A), c ∈ Submonoid.closure {a, b} ↔ ∃ m n, a ^ m * b ^ n = c := by
sorry
This theorem states that for any commutative monoid `A` and any elements `a`, `b`, and `c` in `A`, `c` is an element of the submonoid generated by the two-element set `{a, b}` if and only if there exist integers `m` and `n` such that `a` raised to the power of `m` and `b` raised to the power of `n`, when multiplied together, yield `c`. In other words, `c` can be expressed as a particular "linear combination" of `a` and `b`, where the "coefficients" are exponentiations.
More concisely: For any commutative monoid `A` and elements `a, b, c` in `A`, `c` belongs to the submonoid generated by `{a, b}` if and only if there exist integers `m` and `n` such that `c = a^m * b^n`.
|
Submonoid.iSup_induction'
theorem Submonoid.iSup_induction' :
∀ {M : Type u_1} [inst : MulOneClass M] {ι : Sort u_4} (S : ι → Submonoid M) {C : (x : M) → x ∈ ⨆ i, S i → Prop},
(∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯) →
C 1 ⋯ →
(∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯) →
∀ {x : M} (hx : x ∈ ⨆ i, S i), C x hx
This theorem, `Submonoid.iSup_induction'`, is a dependent version of `Submonoid.iSup_induction`. It's a principle of induction over a superset (_i.e._, the join) of a family of submonoids in a multiplicative structure. It states that for any type `M` with a `MulOneClass` instance, a sort `ι`, and a function `S` from `ι` to submonoids of `M`, we can define a property `C` that depends on an element `x` of `M` and a proof that `x` belongs to the join of the range of `S`. If `C` holds for every element of each `S i`, for the multiplicative identity, and is preserved under multiplication in the join of the range of `S`, then `C` holds for all elements in the join of the range of `S`.
More concisely: If `C` is a property that depends on an element `x` in a multiplicative structure `M` and a proof that `x` belongs to the join of a family of submonoids, and `C` holds for every element in each submonoid, the multiplicative identity, and is preserved under multiplication, then `C` holds for all elements in the join of the submonoids.
|
AddSubmonoid.mem_multiples
theorem AddSubmonoid.mem_multiples : ∀ {M : Type u_1} [inst : AddMonoid M] (n : M), n ∈ AddSubmonoid.multiples n := by
sorry
This theorem states that for any type `M` which has an additive monoid structure, any element `n` of `M` belongs to the additive submonoid generated by `n` itself. In other words, an element is always a member of the set formed by multiplying it by the integers.
More concisely: For any additive monoid `M` and element `n` in `M`, `n` belongs to the additive submonoid generated by `n`.
|
AddSubmonoid.multiset_sum_mem
theorem AddSubmonoid.multiset_sum_mem :
∀ {M : Type u_4} [inst : AddCommMonoid M] (S : AddSubmonoid M) (m : Multiset M), (∀ a ∈ m, a ∈ S) → m.sum ∈ S := by
sorry
This theorem states that for any type `M` which is an additive commutative monoid, given an additive submonoid `S` of `M` and a multiset `m` of elements in `M`, if every element `a` of the multiset `m` belongs to the submonoid `S`, then the sum of all elements in the multiset `m` also belongs to the submonoid `S`. In other words, the sum of a multiset of elements from an additive submonoid of an additive commutative monoid remains in the same additive submonoid.
More concisely: Given an additive commutative monoid `M`, an additive submonoid `S`, and a multiset `m` of elements from `S`, the sum of all elements in `m` belongs to `S`.
|
AddSubmonoid.coe_iSup_of_directed
theorem AddSubmonoid.coe_iSup_of_directed :
∀ {M : Type u_1} [inst : AddZeroClass M] {ι : Sort u_4} [inst_1 : Nonempty ι] {S : ι → AddSubmonoid M},
Directed (fun x x_1 => x ≤ x_1) S → ↑(⨆ i, S i) = ⋃ i, ↑(S i)
The theorem `AddSubmonoid.coe_iSup_of_directed` states that for any type `M` equipped with an `AddZeroClass` structure, any sort `ι` which is nonempty, and any index mapping `S` from `ι` to additive submonoids of `M`, if the given family of submonoids `S` is directed with respect to the `≤` relation, then the union of the carrier sets of all submonoids in the family is equal to the carrier of the supremum of these submonoids. Here, "supremum" (denoted `⨆ i, S i`) is in the sense of complete lattices and the carrier of a submonoid is the set of elements in that submonoid.
More concisely: For any type `M` with an `AddZeroClass` structure, if `ι` is a nonempty sort and `S : ι → additive submonoids of M` is a directed family, then the carrier of the supremum of `S` equals the union of the carriers of all submonoids in `S`.
|
Submonoid.mem_closure_singleton
theorem Submonoid.mem_closure_singleton :
∀ {M : Type u_1} [inst : Monoid M] {x y : M}, y ∈ Submonoid.closure {x} ↔ ∃ n, x ^ n = y
This theorem states that for any type `M` which has a Monoid structure and for any elements `x` and `y` of `M`, `y` is in the submonoid generated by `{x}` if and only if there exists a natural number `n` such that `x` to the power of `n` equals `y`. In other words, the submonoid generated by a single element in a monoid is exactly the set of all natural number powers of that element.
More concisely: For any monoid `M` and element `x` in `M`, the submonoid generated by `{x}` equals the set of all powers of `x` in `M`.
|
multiset_prod_mem
theorem multiset_prod_mem :
∀ {B : Type u_3} {S : B} {M : Type u_4} [inst : CommMonoid M] [inst_1 : SetLike B M] [inst_2 : SubmonoidClass B M]
(m : Multiset M), (∀ a ∈ m, a ∈ S) → m.prod ∈ S
The theorem `multiset_prod_mem` states that for any type `B`, a submonoid `S` of type `B`, a type `M` with a `CommMonoid` structure, and a multiset `m` of elements from `M`, if every element `a` in the multiset `m` is also in the submonoid `S`, then the product of all elements in the multiset `m` (calculated with the `Multiset.prod` function) will also be in the submonoid `S`. This theorem relies on the idea that the product of elements in a submonoid will still be in the submonoid, given a commutative monoid structure on `M`.
More concisely: If `S` is a submonoid of commutative monoid `M`, and all elements in a multiset `m` of `M` belong to `S`, then the multiset product of `m` (as defined in Lean's `Multiset.prod`) is also an element of `S`.
|
AddSubmonoid.list_sum_mem
theorem AddSubmonoid.list_sum_mem :
∀ {M : Type u_1} [inst : AddMonoid M] (s : AddSubmonoid M) {l : List M}, (∀ x ∈ l, x ∈ s) → l.sum ∈ s
This theorem states that the sum of a list of elements in an `AddSubmonoid` is also in the `AddSubmonoid`. More specifically, for any type `M` that has an `AddMonoid` structure, any `AddSubmonoid` `s` of `M`, and any list `l` of elements of `M`, if every element `x` in the list `l` is in `s`, then the sum of all elements in `l` is also in `s`.
More concisely: If `M` is an AddMonoid type, `s` is an AddSubmonoid of `M`, and every element in list `l` of `M` belongs to `s`, then the sum of all elements in `l` also belongs to `s`.
|
AddSubmonoid.iSup_induction
theorem AddSubmonoid.iSup_induction :
∀ {M : Type u_1} [inst : AddZeroClass M] {ι : Sort u_4} (S : ι → AddSubmonoid M) {C : M → Prop} {x : M},
x ∈ ⨆ i, S i → (∀ (i : ι), ∀ x ∈ S i, C x) → C 0 → (∀ (x y : M), C x → C y → C (x + y)) → C x
This theorem, `AddSubmonoid.iSup_induction`, is an induction principle for elements in the supremum of a family of additive submonoids `S i`, indexed by `i`. Suppose we have a property `C` that holds for `0` and for all elements in each `S i` and is preserved under addition. Then, this theorem states that the property `C` holds for any element `x` that lies in the supremum of the `S i`. Therefore, this theorem allows us to extend properties from elements of the individual submonoids to elements of the supremum of the submonoids.
More concisely: If `C` is a property that holds for 0 and is additively closed, then `C` holds for the supremum of any family `{S i}` of additive submonoids if it holds for all elements in each `S i`.
|
sum_mem
theorem sum_mem :
∀ {B : Type u_3} {S : B} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : SetLike B M]
[inst_2 : AddSubmonoidClass B M] {ι : Type u_5} {t : Finset ι} {f : ι → M},
(∀ c ∈ t, f c ∈ S) → (t.sum fun c => f c) ∈ S
This theorem states that the sum of elements in an additive submonoid of an additive commutative monoid, when indexed by a finite set, is also in the same additive submonoid. Specifically, given a type `B` representing the additive submonoid `S` of a type `M` that forms an additive commutative monoid, and given a function `f` that maps elements from a finite set `t` of an arbitrary type `ι` to the monoid `M`, if every element in `t` is mapped to an element in `S` by `f`, then the sum of the mapped elements (i.e., the sum of `f c` for all `c` in `t`) is also an element of `S`.
More concisely: Given an additive submonoid `S` of an additive commutative monoid `M`, and a function `f` mapping a finite set to `M` such that `f(t)` is in `S` for all `t` in the set, then the sum of `f(t)` for all `t` in the set is also in `S`.
|
MulMemClass.mul_right_mem_add_closure
theorem MulMemClass.mul_right_mem_add_closure :
∀ {M : Type u_1} {R : Type u_4} [inst : NonUnitalNonAssocSemiring R] [inst_1 : SetLike M R]
[inst_2 : MulMemClass M R] {S : M} {a b : R},
a ∈ AddSubmonoid.closure ↑S → b ∈ S → a * b ∈ AddSubmonoid.closure ↑S
The theorem `MulMemClass.mul_right_mem_add_closure` states that for any type `M` and `R` where `R` forms a non-unital non-associative semiring and `M` is a set-like structure in `R` following the `MulMemClass` property (such that multiplication of any two elements in `M` stays within `M`), if `S` is a set in `M` and `a` and `b` are elements in `R`, then, if `a` belongs to the additive closure of `S` and `b` belongs to `S`, the product of `a` and `b` would also be an element of the additive closure of `S`. In simple terms, it implies that the product of an element from the additive closure of a subsemigroup and an element from that subsemigroup stays within the additive closure of that subsemigroup.
More concisely: If `M` is a set-like structure in a non-unital non-associative semiring `R` with `MulMemClass` property, and `S` is a subset of `M` with `a` in the additive closure of `S` and `b` in `S`, then `a * b` is in the additive closure of `S`.
|
AddSubmonoid.mem_closure_pair
theorem AddSubmonoid.mem_closure_pair :
∀ {A : Type u_4} [inst : AddCommMonoid A] (a b c : A), c ∈ AddSubmonoid.closure {a, b} ↔ ∃ m n, m • a + n • b = c
This theorem states that for any type `A` that is an additive commutative monoid and any elements `a`, `b`, and `c` of `A`, `c` is in the additive submonoid generated by the set containing `a` and `b` if and only if there exist integers `m` and `n` such that `m` times `a` plus `n` times `b` equals `c`. In other words, an element is in the closure of a two-element set in an additive commutative monoid if and only if it is a linear combination of those two elements.
More concisely: For any additive commutative monoid `A` and elements `a, b, c` in `A`, `c` belongs to the additive submonoid generated by `{a, b}` if and only if there exist integers `m` and `n` such that `m * a + n * b = c`.
|
Submonoid.prod_mem
theorem Submonoid.prod_mem :
∀ {M : Type u_4} [inst : CommMonoid M] (S : Submonoid M) {ι : Type u_5} {t : Finset ι} {f : ι → M},
(∀ c ∈ t, f c ∈ S) → (t.prod fun c => f c) ∈ S
This theorem states that for any commutative monoid `M` and its submonoid `S`, any finitely-indexed product of elements from `S` is also in `S`. More precisely, given a function `f` mapping indices of type `ι` to elements of `M`, if for every element `c` in a finite set `t` the function `f` maps `c` to an element in `S`, then the product, over all `c` in `t`, of `f(c)` is also an element of the submonoid `S`. This result essentially captures the closure property of submonoids in the context of finite products.
More concisely: Given a commutative monoid `M` and its submonoid `S`, any finite product of elements from `S` is also in `S`.
|
AddSubmonoid.iSup_induction'
theorem AddSubmonoid.iSup_induction' :
∀ {M : Type u_1} [inst : AddZeroClass M] {ι : Sort u_4} (S : ι → AddSubmonoid M)
{C : (x : M) → x ∈ ⨆ i, S i → Prop},
(∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯) →
C 0 ⋯ →
(∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x + y) ⋯) →
∀ {x : M} (hx : x ∈ ⨆ i, S i), C x hx
This theorem is a dependent version of `AddSubmonoid.iSup_induction`. Given a type `M` with an instance of `AddZeroClass`, an indexing type `ι`, and a function `S` mapping `ι` to `AddSubmonoid` of `M`, it states that for a property `C` that holds for all elements `x` in the supremum of `S i` over all `i`, if `C` holds for all `x` in each `S i`, `C` holds for `0`, and `C` holds for the sum of any two elements in the supremum of `S i` given that `C` holds for each of them, then `C` holds for any element `x` in the supremum of `S i`.
More concisely: If `S : ι → AddSubmonoid M` has the property that the supremum of `S` satisfies `AddZeroClass`, and `C` holds for all elements in each `S i` and for `0`, and `C` is closed under addition of elements in the supremum of `S`, then `C` holds for every element in the supremum of `S`.
|
Submonoid.powers_le
theorem Submonoid.powers_le :
∀ {M : Type u_1} [inst : Monoid M] {n : M} {P : Submonoid M}, Submonoid.powers n ≤ P ↔ n ∈ P
This theorem, `Submonoid.powers_le`, states that for any type `M` equipped with a monoid structure, any element `n` of `M`, and any submonoid `P` of `M`, the submonoid generated by `n` (i.e., the set of all powers of `n`) is a subset of `P` if and only if `n` is an element of `P`. In other words, in any monoid, an element generates a submonoid that is contained within another submonoid if and only if the element is a member of the second submonoid.
More concisely: In a monoid, an element generates a submonoid contained within another if and only if the element is a member of that submonoid.
|