# Submonoids: membership criteria for products and sums #

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;

## Tags #

submonoid, submonoids

source
@[simp]
theorem SubmonoidClass.coe_list_prod {M : Type u_1} {B : Type u_3} [Monoid M] [SetLike B M] [SubmonoidClass B M] {S : B} (l : List ↥S) :
↑l.prod = (List.map Subtype.val l).prod
source
@[simp]
theorem AddSubmonoidClass.coe_list_sum {M : Type u_1} {B : Type u_3} [AddMonoid M] [SetLike B M] [AddSubmonoidClass B M] {S : B} (l : List ↥S) :
↑l.sum = (List.map Subtype.val l).sum
source
@[simp]
theorem SubmonoidClass.coe_multiset_prod {B : Type u_3} {S : B} {M : Type u_4} [CommMonoid M] [SetLike B M] [SubmonoidClass B M] (m : Multiset ↥S) :
↑m.prod = (Multiset.map Subtype.val m).prod
source
@[simp]
theorem AddSubmonoidClass.coe_multiset_sum {B : Type u_3} {S : B} {M : Type u_4} [AddCommMonoid M] [SetLike B M] [AddSubmonoidClass B M] (m : Multiset ↥S) :
↑m.sum = (Multiset.map Subtype.val m).sum
source
@[simp]
theorem SubmonoidClass.coe_finset_prod {B : Type u_3} {S : B} {ι : Type u_4} {M : Type u_5} [CommMonoid M] [SetLike B M] [SubmonoidClass B M] (f : ι → ↥S) (s : Finset ι) :
↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
source
@[simp]
theorem AddSubmonoidClass.coe_finset_sum {B : Type u_3} {S : B} {ι : Type u_4} {M : Type u_5} [AddCommMonoid M] [SetLike B M] [AddSubmonoidClass B M] (f : ι → ↥S) (s : Finset ι) :
↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
source
theorem list_prod_mem {M : Type u_1} {B : Type u_3} [Monoid M] [SetLike B M] [SubmonoidClass B M] {S : B} {l : List M} (hl : ∀ x ∈ l, x ∈ S) :
l.prod ∈ S

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

source
theorem list_sum_mem {M : Type u_1} {B : Type u_3} [AddMonoid M] [SetLike B M] [AddSubmonoidClass B M] {S : B} {l : List M} (hl : ∀ x ∈ l, x ∈ S) :
l.sum ∈ S

Sum of a list of elements in an `AddSubmonoid` is in the `AddSubmonoid`.

source
theorem multiset_prod_mem {B : Type u_3} {S : B} {M : Type u_4} [CommMonoid M] [SetLike B M] [SubmonoidClass B M] (m : Multiset M) (hm : ∀ a ∈ m, a ∈ S) :
m.prod ∈ S

Product of a multiset of elements in a submonoid of a `CommMonoid` is in the submonoid.

source
theorem multiset_sum_mem {B : Type u_3} {S : B} {M : Type u_4} [AddCommMonoid M] [SetLike B M] [AddSubmonoidClass B M] (m : Multiset M) (hm : ∀ a ∈ m, a ∈ S) :
m.sum ∈ S

Sum of a multiset of elements in an `AddSubmonoid` of an `AddCommMonoid` is in the `AddSubmonoid`.

source
theorem prod_mem {B : Type u_3} {S : B} {M : Type u_4} [CommMonoid M] [SetLike B M] [SubmonoidClass B M] {ι : Type u_5} {t : Finset ι} {f : ι → M} (h : ∀ c ∈ t, f c ∈ S) :
∏ c ∈ t, f c ∈ S

Product of elements of a submonoid of a `CommMonoid` indexed by a `Finset` is in the submonoid.

source
theorem sum_mem {B : Type u_3} {S : B} {M : Type u_4} [AddCommMonoid M] [SetLike B M] [AddSubmonoidClass B M] {ι : Type u_5} {t : Finset ι} {f : ι → M} (h : ∀ c ∈ t, f c ∈ S) :
∑ c ∈ t, f c ∈ S

Sum of elements in an `AddSubmonoid` of an `AddCommMonoid` indexed by a `Finset` is in the `AddSubmonoid`.

source
theorem Submonoid.coe_list_prod {M : Type u_1} [Monoid M] (s : Submonoid M) (l : List ↥s) :
↑l.prod = (List.map Subtype.val l).prod
source
theorem AddSubmonoid.coe_list_sum {M : Type u_1} [AddMonoid M] (s : AddSubmonoid M) (l : List ↥s) :
↑l.sum = (List.map Subtype.val l).sum
source
theorem Submonoid.coe_multiset_prod {M : Type u_4} [CommMonoid M] (S : Submonoid M) (m : Multiset ↥S) :
↑m.prod = (Multiset.map Subtype.val m).prod
source
theorem AddSubmonoid.coe_multiset_sum {M : Type u_4} [AddCommMonoid M] (S : AddSubmonoid M) (m : Multiset ↥S) :
↑m.sum = (Multiset.map Subtype.val m).sum
source
theorem Submonoid.coe_finset_prod {ι : Type u_4} {M : Type u_5} [CommMonoid M] (S : Submonoid M) (f : ι → ↥S) (s : Finset ι) :
↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
source
theorem AddSubmonoid.coe_finset_sum {ι : Type u_4} {M : Type u_5} [AddCommMonoid M] (S : AddSubmonoid M) (f : ι → ↥S) (s : Finset ι) :
↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
source
theorem Submonoid.list_prod_mem {M : Type u_1} [Monoid M] (s : Submonoid M) {l : List M} (hl : ∀ x ∈ l, x ∈ s) :
l.prod ∈ s

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

source
theorem AddSubmonoid.list_sum_mem {M : Type u_1} [AddMonoid M] (s : AddSubmonoid M) {l : List M} (hl : ∀ x ∈ l, x ∈ s) :
l.sum ∈ s

Sum of a list of elements in an `AddSubmonoid` is in the `AddSubmonoid`.

source
theorem Submonoid.multiset_prod_mem {M : Type u_4} [CommMonoid M] (S : Submonoid M) (m : Multiset M) (hm : ∀ a ∈ m, a ∈ S) :
m.prod ∈ S

Product of a multiset of elements in a submonoid of a `CommMonoid` is in the submonoid.

source
theorem AddSubmonoid.multiset_sum_mem {M : Type u_4} [AddCommMonoid M] (S : AddSubmonoid M) (m : Multiset M) (hm : ∀ a ∈ m, a ∈ S) :
m.sum ∈ S

Sum of a multiset of elements in an `AddSubmonoid` of an `AddCommMonoid` is in the `AddSubmonoid`.

source
theorem Submonoid.multiset_noncommProd_mem {M : Type u_1} [Monoid M] (S : Submonoid M) (m : Multiset M) (comm : {x : M | x ∈ m}.Pairwise Commute) (h : ∀ x ∈ m, x ∈ S) :
m.noncommProd comm ∈ S
source
theorem AddSubmonoid.multiset_noncommSum_mem {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (m : Multiset M) (comm : {x : M | x ∈ m}.Pairwise AddCommute) (h : ∀ x ∈ m, x ∈ S) :
m.noncommSum comm ∈ S
source
theorem Submonoid.prod_mem {M : Type u_4} [CommMonoid M] (S : Submonoid M) {ι : Type u_5} {t : Finset ι} {f : ι → M} (h : ∀ c ∈ t, f c ∈ S) :
∏ c ∈ t, f c ∈ S

Product of elements of a submonoid of a `CommMonoid` indexed by a `Finset` is in the submonoid.

source
theorem AddSubmonoid.sum_mem {M : Type u_4} [AddCommMonoid M] (S : AddSubmonoid M) {ι : Type u_5} {t : Finset ι} {f : ι → M} (h : ∀ c ∈ t, f c ∈ S) :
∑ c ∈ t, f c ∈ S

Sum of elements in an `AddSubmonoid` of an `AddCommMonoid` indexed by a `Finset` is in the `AddSubmonoid`.

source
theorem Submonoid.noncommProd_mem {M : Type u_1} [Monoid M] (S : Submonoid M) {ι : Type u_4} (t : Finset ι) (f : ι → M) (comm : (↑t).Pairwise (Function.onFun Commute f)) (h : ∀ c ∈ t, f c ∈ S) :
t.noncommProd f comm ∈ S
source
theorem AddSubmonoid.noncommSum_mem {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {ι : Type u_4} (t : Finset ι) (f : ι → M) (comm : (↑t).Pairwise (Function.onFun AddCommute f)) (h : ∀ c ∈ t, f c ∈ S) :
t.noncommSum f comm ∈ S
source
theorem Submonoid.mem_closure_iff_exists_finset_subset {M : Type u_1} [CommMonoid M] {x : M} {s : Set M} :
x ∈ closure s ↔ ∃ (f : M → ℕ) (t : Finset M), ↑t ⊆ s ∧ Function.support f ⊆ ↑t ∧ ∏ a ∈ t, a ^ f a = x
source
theorem AddSubmonoid.mem_closure_iff_exists_finset_subset {M : Type u_1} [AddCommMonoid M] {x : M} {s : Set M} :
x ∈ closure s ↔ ∃ (f : M → ℕ) (t : Finset M), ↑t ⊆ s ∧ Function.support f ⊆ ↑t ∧ ∑ a ∈ t, f a • a = x
source
theorem Submonoid.mem_closure_finset {M : Type u_1} [CommMonoid M] {x : M} {s : Finset M} :
x ∈ closure ↑s ↔ ∃ (f : M → ℕ), Function.support f ⊆ ↑s ∧ ∏ a ∈ s, a ^ f a = x
source
theorem AddSubmonoid.mem_closure_finset {M : Type u_1} [AddCommMonoid M] {x : M} {s : Finset M} :
x ∈ closure ↑s ↔ ∃ (f : M → ℕ), Function.support f ⊆ ↑s ∧ ∑ a ∈ s, f a • a = x