# mathlibdocumentation

group_theory.submonoid.membership

# Submonoids: membership criteria

In this file we prove various facts about membership in a submonoid:

• list_prod_mem, multiset_prod_mem, prod_mem: if each element of a collection belongs to a multiplicative submonoid, then so does their product;
• list_sum_mem, multiset_sum_mem, sum_mem: if each element of a collection belongs to an additive submonoid, then so does their sum;
• pow_mem, nsmul_mem: if x ∈ S where S is a multiplicative (resp., additive) submonoid and n is a natural number, then x^n (resp., n •ℕ x) belongs to S;
• mem_supr_of_directed, coe_supr_of_directed, mem_Sup_of_directed_on, coe_Sup_of_directed_on: the supremum of a directed collection of submonoid is their union.
• sup_eq_range, mem_sup: supremum of two submonoids S, T of a commutative monoid is the set of products;
• closure_singleton_eq, mem_closure_singleton: the multiplicative (resp., additive) closure of {x} consists of powers (resp., natural multiples) of x.

## Tags

submonoid, submonoids

theorem submonoid.list_prod_mem {M : Type u_1} [monoid M] (S : submonoid M) {l : list M} :
(∀ (x : M), x lx S)l.prod S

Product of a list of elements in a submonoid is in the submonoid.

theorem add_submonoid.list_sum_mem {M : Type u_1} [add_monoid M] (S : add_submonoid M) {l : list M} :
(∀ (x : M), x lx S)l.sum S

Sum of a list of elements in an add_submonoid is in the add_submonoid.

theorem submonoid.multiset_prod_mem {M : Type u_1} [comm_monoid M] (S : submonoid M) (m : multiset M) :
(∀ (a : M), a ma S)m.prod S

Product of a multiset of elements in a submonoid of a comm_monoid is in the submonoid.

theorem add_submonoid.multiset_sum_mem {M : Type u_1} (S : add_submonoid M) (m : multiset M) :
(∀ (a : M), a ma S)m.sum S

Sum of a multiset of elements in an add_submonoid of an add_comm_monoid is in the add_submonoid.

theorem add_submonoid.sum_mem {M : Type u_1} (S : add_submonoid M) {ι : Type u_2} {t : finset ι} {f : ι → M} :
(∀ (c : ι), c tf c S)∑ (c : ι) in t, f c S

Sum of elements in an add_submonoid of an add_comm_monoid indexed by a finset is in the add_submonoid.

theorem submonoid.prod_mem {M : Type u_1} [comm_monoid M] (S : submonoid M) {ι : Type u_2} {t : finset ι} {f : ι → M} :
(∀ (c : ι), c tf c S)∏ (c : ι) in t, f c S

Product of elements of a submonoid of a comm_monoid indexed by a finset is in the submonoid.

theorem submonoid.pow_mem {M : Type u_1} [monoid M] (S : submonoid M) {x : M} (hx : x S) (n : ) :
x ^ n S

theorem add_submonoid.mem_supr_of_directed {M : Type u_1} [add_monoid M] {ι : Sort u_2} [hι : nonempty ι] {S : ι → } (hS : S) {x : M} :
(x ⨆ (i : ι), S i) ∃ (i : ι), x S i

theorem submonoid.mem_supr_of_directed {M : Type u_1} [monoid M] {ι : Sort u_2} [hι : nonempty ι] {S : ι → } (hS : S) {x : M} :
(x ⨆ (i : ι), S i) ∃ (i : ι), x S i

theorem add_submonoid.coe_supr_of_directed {M : Type u_1} [add_monoid M] {ι : Sort u_2} [nonempty ι] {S : ι → } :
((⨆ (i : ι), S i) = ⋃ (i : ι), (S i))

theorem submonoid.coe_supr_of_directed {M : Type u_1} [monoid M] {ι : Sort u_2} [nonempty ι] {S : ι → } :
((⨆ (i : ι), S i) = ⋃ (i : ι), (S i))

theorem submonoid.mem_Sup_of_directed_on {M : Type u_1} [monoid M] {S : set (submonoid M)} (Sne : S.nonempty) (hS : S) {x : M} :
x Sup S ∃ (s : (H : s S), x s

theorem add_submonoid.mem_Sup_of_directed_on {M : Type u_1} [add_monoid M] {S : set } (Sne : S.nonempty) (hS : S) {x : M} :
x Sup S ∃ (s : (H : s S), x s

theorem add_submonoid.coe_Sup_of_directed_on {M : Type u_1} [add_monoid M] {S : set } :
S.nonempty((Sup S) = ⋃ (s : (H : s S), s)

theorem submonoid.coe_Sup_of_directed_on {M : Type u_1} [monoid M] {S : set (submonoid M)} :
S.nonempty((Sup S) = ⋃ (s : (H : s S), s)

theorem submonoid.mem_sup_left {M : Type u_1} [monoid M] {S T : submonoid M} {x : M} :
x Sx S T

theorem add_submonoid.mem_sup_left {M : Type u_1} [add_monoid M] {S T : add_submonoid M} {x : M} :
x Sx S T

theorem submonoid.mem_sup_right {M : Type u_1} [monoid M] {S T : submonoid M} {x : M} :
x Tx S T

theorem add_submonoid.mem_sup_right {M : Type u_1} [add_monoid M] {S T : add_submonoid M} {x : M} :
x Tx S T

theorem submonoid.mem_supr_of_mem {M : Type u_1} [monoid M] {ι : Type u_2} {S : ι → } (i : ι) {x : M} :
x S ix supr S

theorem add_submonoid.mem_supr_of_mem {M : Type u_1} [add_monoid M] {ι : Type u_2} {S : ι → } (i : ι) {x : M} :
x S ix supr S

theorem add_submonoid.mem_Sup_of_mem {M : Type u_1} [add_monoid M] {S : set } {s : add_submonoid M} (hs : s S) {x : M} :
x sx Sup S

theorem submonoid.mem_Sup_of_mem {M : Type u_1} [monoid M] {S : set (submonoid M)} {s : submonoid M} (hs : s S) {x : M} :
x sx Sup S

theorem free_monoid.closure_range_of {α : Type u_3} :

theorem free_add_monoid.closure_range_of {α : Type u_3} :

theorem submonoid.closure_singleton_eq {M : Type u_1} [monoid M] (x : M) :

theorem submonoid.mem_closure_singleton {M : Type u_1} [monoid M] {x y : M} :
y ∃ (n : ), x ^ n = y

The submonoid generated by an element of a monoid equals the set of natural number powers of the element.

theorem submonoid.mem_closure_singleton_self {M : Type u_1} [monoid M] {y : M} :
y

theorem submonoid.closure_singleton_one {M : Type u_1} [monoid M] :

theorem submonoid.closure_eq_mrange {M : Type u_1} [monoid M] (s : set M) :

theorem add_submonoid.closure_eq_mrange {M : Type u_1} [add_monoid M] (s : set M) :

theorem submonoid.exists_list_of_mem_closure {M : Type u_1} [monoid M] {s : set M} {x : M} :
(∃ (l : list M) (hl : ∀ (y : M), y ly s), l.prod = x)

theorem add_submonoid.exists_list_of_mem_closure {M : Type u_1} [add_monoid M] {s : set M} {x : M} :
(∃ (l : list M) (hl : ∀ (y : M), y ly s), l.sum = x)

def submonoid.powers {N : Type u_3} [monoid N] :
N →

The submonoid generated by an element.

Equations
@[simp]
theorem submonoid.mem_powers {N : Type u_3} [monoid N] (n : N) :

theorem submonoid.powers_eq_closure {N : Type u_3} [monoid N] (n : N) :

theorem submonoid.powers_subset {N : Type u_3} [monoid N] {n : N} {P : submonoid N} :
n P

theorem add_submonoid.sup_eq_range {N : Type u_3} (s t : add_submonoid N) :

theorem submonoid.sup_eq_range {N : Type u_3} [comm_monoid N] (s t : submonoid N) :

theorem submonoid.mem_sup {N : Type u_3} [comm_monoid N] {s t : submonoid N} {x : N} :
x s t ∃ (y : N) (H : y s) (z : N) (H : z t), y * z = x

theorem add_submonoid.mem_sup {N : Type u_3} {s t : add_submonoid N} {x : N} :
x s t ∃ (y : N) (H : y s) (z : N) (H : z t), y + z = x

theorem add_submonoid.nsmul_mem {A : Type u_2} [add_monoid A] (S : add_submonoid A) {x : A} (hx : x S) (n : ) :
n •ℕ x S

theorem add_submonoid.closure_singleton_eq {A : Type u_2} [add_monoid A] (x : A) :
= ( x).mrange

theorem add_submonoid.mem_closure_singleton {A : Type u_2} [add_monoid A] {x y : A} :
∃ (n : ), n •ℕ x = y

The add_submonoid generated by an element of an add_monoid equals the set of natural number multiples of the element.