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

@[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

@[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

@[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

@[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

@[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)

@[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)

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.

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.

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.

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.

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.

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.

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

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

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

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

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)

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)

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.

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.

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.

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.

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

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

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.

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.

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

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

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

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

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

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