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: ifx ∈ SwhereSis a multiplicative (resp., additive) submonoid andnis a natural number, thenx^n(resp.,n •ℕ x) belongs toS;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 submonoidsS,Tof 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) ofx.
Tags
submonoid, submonoids
theorem
add_submonoid.list_sum_mem
{M : Type u_1}
[add_monoid M]
(S : add_submonoid M)
{l : list M} :
Sum of a list of elements in an add_submonoid is in the add_submonoid.
theorem
add_submonoid.multiset_sum_mem
{M : Type u_1}
[add_comm_monoid M]
(S : add_submonoid M)
(m : multiset M) :
Sum of a multiset of elements in an add_submonoid of an add_comm_monoid is
in the add_submonoid.
theorem
submonoid.multiset_prod_mem
{M : Type u_1}
[comm_monoid M]
(S : submonoid M)
(m : multiset M) :
Product of a multiset of elements in a submonoid of a comm_monoid is in the submonoid.
theorem
add_submonoid.sum_mem
{M : Type u_1}
[add_comm_monoid M]
(S : add_submonoid M)
{ι : Type u_2}
{t : finset ι}
{f : ι → M} :
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} :
Product of elements of a submonoid of a comm_monoid indexed by a finset is in the
submonoid.
theorem
add_submonoid.mem_supr_of_directed
{M : Type u_1}
[add_monoid M]
{ι : Sort u_2}
[hι : nonempty ι]
{S : ι → add_submonoid M}
(hS : directed has_le.le S)
{x : M} :
theorem
add_submonoid.coe_supr_of_directed
{M : Type u_1}
[add_monoid M]
{ι : Sort u_2}
[nonempty ι]
{S : ι → add_submonoid M} :
theorem
add_submonoid.mem_Sup_of_directed_on
{M : Type u_1}
[add_monoid M]
{S : set (add_submonoid M)}
(Sne : S.nonempty)
(hS : directed_on has_le.le S)
{x : M} :
x ∈ has_Sup.Sup S ↔ ∃ (s : add_submonoid M) (H : s ∈ S), x ∈ s
theorem
submonoid.mem_Sup_of_directed_on
{M : Type u_1}
[monoid M]
{S : set (submonoid M)}
(Sne : S.nonempty)
(hS : directed_on has_le.le S)
{x : M} :
theorem
submonoid.coe_Sup_of_directed_on
{M : Type u_1}
[monoid M]
{S : set (submonoid M)} :
S.nonempty → directed_on has_le.le S → (↑(has_Sup.Sup S) = ⋃ (s : submonoid M) (H : s ∈ S), ↑s)
theorem
add_submonoid.coe_Sup_of_directed_on
{M : Type u_1}
[add_monoid M]
{S : set (add_submonoid M)} :
S.nonempty → directed_on has_le.le S → (↑(has_Sup.Sup S) = ⋃ (s : add_submonoid M) (H : s ∈ S), ↑s)
theorem
add_submonoid.mem_sup_right
{M : Type u_1}
[add_monoid M]
{S T : add_submonoid M}
{x : M} :
theorem
add_submonoid.mem_supr_of_mem
{M : Type u_1}
[add_monoid M]
{ι : Type u_2}
{S : ι → add_submonoid M}
(i : ι)
{x : M} :
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 ∈ s → x ∈ has_Sup.Sup S
theorem
add_submonoid.mem_Sup_of_mem
{M : Type u_1}
[add_monoid M]
{S : set (add_submonoid M)}
{s : add_submonoid M}
(hs : s ∈ S)
{x : M} :
x ∈ s → x ∈ has_Sup.Sup S
theorem
submonoid.closure_singleton_eq
{M : Type u_1}
[monoid M]
(x : M) :
submonoid.closure {x} = (⇑(powers_hom M) x).mrange
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 ∈ submonoid.closure {y}
theorem
add_submonoid.exists_list_of_mem_closure
{M : Type u_1}
[add_monoid M]
{s : set M}
{x : M} :
The submonoid generated by an element.
Equations
- submonoid.powers n = (⇑(powers_hom N) n).mrange.copy (set.range (has_pow.pow n)) _
@[simp]
theorem
submonoid.powers_subset
{N : Type u_3}
[monoid N]
{n : N}
{P : submonoid N} :
n ∈ P → submonoid.powers n ≤ P
theorem
add_submonoid.nsmul_mem
{A : Type u_2}
[add_monoid A]
(S : add_submonoid A)
{x : A}
(hx : x ∈ S)
(n : ℕ) :
theorem
add_submonoid.closure_singleton_eq
{A : Type u_2}
[add_monoid A]
(x : A) :
add_submonoid.closure {x} = (⇑(multiples_hom A) x).mrange
The add_submonoid generated by an element of an add_monoid equals the set of
natural number multiples of the element.
The additive submonoid generated by an element.
Equations
- add_submonoid.multiples x = (⇑(multiples_hom A) x).mrange.copy (set.range (λ (i : ℕ), i •ℕ x)) _
@[simp]
theorem
add_submonoid.multiples_subset
{A : Type u_2}
[add_monoid A]
{x : A}
{P : add_submonoid A} :
x ∈ P → add_submonoid.multiples x ≤ P