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)
:
@[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)
:
@[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_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
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
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
AddSubmonoid.noncommSum_mem
{M : Type u_1}
[AddMonoid M]
(S : AddSubmonoid M)
{ι : Type u_4}
(t : Finset ι)
(f : ι → M)
(comm : (↑t).Pairwise (AddCommute on f))
(h : ∀ c ∈ t, f c ∈ S)
:
t.noncommSum f comm ∈ S