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_2}
[Monoid M]
[SetLike B M]
[SubmonoidClass B M]
{S : B}
(l : List ↥S)
:
@[simp]
theorem
AddSubmonoidClass.coe_list_sum
{M : Type u_1}
{B : Type u_2}
[AddMonoid M]
[SetLike B M]
[AddSubmonoidClass B M]
{S : B}
(l : List ↥S)
:
@[simp]
theorem
SubmonoidClass.coe_multiset_prod
{B : Type u_2}
{S : B}
{M : Type u_3}
[CommMonoid M]
[SetLike B M]
[SubmonoidClass B M]
(m : Multiset ↥S)
:
@[simp]
theorem
AddSubmonoidClass.coe_multiset_sum
{B : Type u_2}
{S : B}
{M : Type u_3}
[AddCommMonoid M]
[SetLike B M]
[AddSubmonoidClass B M]
(m : Multiset ↥S)
:
@[simp]
theorem
SubmonoidClass.coe_finsetProd
{B : Type u_2}
{S : B}
{ι : Type u_3}
{M : Type u_4}
[CommMonoid M]
[SetLike B M]
[SubmonoidClass B M]
(f : ι → ↥S)
(s : Finset ι)
:
@[simp]
theorem
AddSubmonoidClass.coe_finsetSum
{B : Type u_2}
{S : B}
{ι : Type u_3}
{M : Type u_4}
[AddCommMonoid M]
[SetLike B M]
[AddSubmonoidClass B M]
(f : ι → ↥S)
(s : Finset ι)
:
@[deprecated AddSubmonoidClass.coe_finsetSum (since := "2026-04-08")]
theorem
AddSubmonoidClass.coe_finset_sum
{B : Type u_2}
{S : B}
{ι : Type u_3}
{M : Type u_4}
[AddCommMonoid M]
[SetLike B M]
[AddSubmonoidClass B M]
(f : ι → ↥S)
(s : Finset ι)
:
Alias of AddSubmonoidClass.coe_finsetSum.
@[deprecated SubmonoidClass.coe_finsetProd (since := "2026-04-08")]
theorem
SubmonoidClass.coe_finset_prod
{B : Type u_2}
{S : B}
{ι : Type u_3}
{M : Type u_4}
[CommMonoid M]
[SetLike B M]
[SubmonoidClass B M]
(f : ι → ↥S)
(s : Finset ι)
:
Alias of SubmonoidClass.coe_finsetProd.
theorem
list_sum_mem
{M : Type u_1}
{B : Type u_2}
[AddMonoid M]
[SetLike B M]
[AddSubmonoidClass B M]
{S : B}
{l : List M}
(hl : ∀ x ∈ l, x ∈ S)
:
Sum of a list of elements in an AddSubmonoid is in the AddSubmonoid.
theorem
multiset_prod_mem
{B : Type u_2}
{S : B}
{M : Type u_3}
[CommMonoid M]
[SetLike B M]
[SubmonoidClass B M]
(m : Multiset M)
(hm : ∀ a ∈ m, a ∈ S)
:
Product of a multiset of elements in a submonoid of a CommMonoid is in the submonoid.
theorem
multiset_sum_mem
{B : Type u_2}
{S : B}
{M : Type u_3}
[AddCommMonoid M]
[SetLike B M]
[AddSubmonoidClass B M]
(m : Multiset M)
(hm : ∀ a ∈ m, a ∈ S)
:
Sum of a multiset of elements in an AddSubmonoid of an AddCommMonoid is
in the AddSubmonoid.
theorem
prod_mem
{B : Type u_2}
{S : B}
{M : Type u_3}
[CommMonoid M]
[SetLike B M]
[SubmonoidClass B M]
{ι : Type u_4}
{t : Finset ι}
{f : ι → M}
(h : ∀ 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_2}
{S : B}
{M : Type u_3}
[AddCommMonoid M]
[SetLike B M]
[AddSubmonoidClass B M]
{ι : Type u_4}
{t : Finset ι}
{f : ι → M}
(h : ∀ 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_multiset_prod
{M : Type u_3}
[CommMonoid M]
(S : Submonoid M)
(m : Multiset ↥S)
:
theorem
AddSubmonoid.coe_multiset_sum
{M : Type u_3}
[AddCommMonoid M]
(S : AddSubmonoid M)
(m : Multiset ↥S)
:
theorem
Submonoid.coe_finsetProd
{ι : Type u_3}
{M : Type u_4}
[CommMonoid M]
(S : Submonoid M)
(f : ι → ↥S)
(s : Finset ι)
:
theorem
AddSubmonoid.coe_finsetSum
{ι : Type u_3}
{M : Type u_4}
[AddCommMonoid M]
(S : AddSubmonoid M)
(f : ι → ↥S)
(s : Finset ι)
:
@[deprecated AddSubmonoid.coe_finsetSum (since := "2026-04-08")]
theorem
AddSubmonoid.coe_finset_sum
{ι : Type u_3}
{M : Type u_4}
[AddCommMonoid M]
(S : AddSubmonoid M)
(f : ι → ↥S)
(s : Finset ι)
:
Alias of AddSubmonoid.coe_finsetSum.
@[deprecated Submonoid.coe_finsetProd (since := "2026-04-08")]
theorem
Submonoid.coe_finset_prod
{ι : Type u_3}
{M : Type u_4}
[CommMonoid M]
(S : Submonoid M)
(f : ι → ↥S)
(s : Finset ι)
:
Alias of Submonoid.coe_finsetProd.
theorem
AddSubmonoid.list_sum_mem
{M : Type u_1}
[AddMonoid M]
(s : AddSubmonoid M)
{l : List M}
(hl : ∀ x ∈ l, x ∈ s)
:
Sum of a list of elements in an AddSubmonoid is in the AddSubmonoid.
theorem
Submonoid.multiset_prod_mem
{M : Type u_3}
[CommMonoid M]
(S : Submonoid M)
(m : Multiset M)
(hm : ∀ a ∈ m, a ∈ 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_3}
[AddCommMonoid M]
(S : AddSubmonoid M)
(m : Multiset M)
(hm : ∀ a ∈ m, a ∈ S)
:
Sum of a multiset of elements in an AddSubmonoid of an AddCommMonoid is
in the AddSubmonoid.
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)
:
theorem
Submonoid.prod_mem
{M : Type u_3}
[CommMonoid M]
(S : Submonoid M)
{ι : Type u_4}
{t : Finset ι}
{f : ι → M}
(h : ∀ 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_3}
[AddCommMonoid M]
(S : AddSubmonoid M)
{ι : Type u_4}
{t : Finset ι}
{f : ι → M}
(h : ∀ 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_3}
(t : Finset ι)
(f : ι → M)
(comm : (↑t).Pairwise (Function.onFun Commute f))
(h : ∀ c ∈ t, f c ∈ S)
:
theorem
AddSubmonoid.noncommSum_mem
{M : Type u_1}
[AddMonoid M]
(S : AddSubmonoid M)
{ι : Type u_3}
(t : Finset ι)
(f : ι → M)
(comm : (↑t).Pairwise (Function.onFun AddCommute f))
(h : ∀ c ∈ t, f c ∈ S)
:
theorem
Submonoid.mem_closure_iff_exists_finset_subset
{M : Type u_1}
[CommMonoid M]
{x : M}
{s : Set M}
:
theorem
AddSubmonoid.mem_closure_iff_exists_finset_subset
{M : Type u_1}
[AddCommMonoid M]
{x : M}
{s : Set M}
: