Sums and products over multisets #
In this file we define products and sums indexed by multisets. This is later used to define products and sums indexed by finite sets.
Main declarations #
Multiset.prod
:s.prod f
is the product off i
over alli ∈ s
. Not to be mistaken with the cartesian productMultiset.product
.Multiset.sum
:s.sum f
is the sum off i
over alli ∈ s
.
@[simp]
theorem
Multiset.prod_erase
{M : Type u_5}
[CommMonoid M]
{s : Multiset M}
{a : M}
[DecidableEq M]
(h : a ∈ s)
:
@[simp]
theorem
Multiset.sum_erase
{M : Type u_5}
[AddCommMonoid M]
{s : Multiset M}
{a : M}
[DecidableEq M]
(h : a ∈ s)
:
@[simp]
theorem
Multiset.prod_map_erase
{ι : Type u_2}
{M : Type u_5}
[CommMonoid M]
{m : Multiset ι}
{f : ι → M}
[DecidableEq ι]
{a : ι}
(h : a ∈ m)
:
@[simp]
theorem
Multiset.sum_map_erase
{ι : Type u_2}
{M : Type u_5}
[AddCommMonoid M]
{m : Multiset ι}
{f : ι → M}
[DecidableEq ι]
{a : ι}
(h : a ∈ m)
:
theorem
Multiset.prod_filter_mul_prod_filter_not
{M : Type u_5}
[CommMonoid M]
{s : Multiset M}
(p : M → Prop)
[DecidablePred p]
:
theorem
Multiset.sum_filter_add_sum_filter_not
{M : Type u_5}
[AddCommMonoid M]
{s : Multiset M}
(p : M → Prop)
[DecidablePred p]
:
theorem
Multiset.prod_map_eq_pow_single
{ι : Type u_2}
{M : Type u_5}
[CommMonoid M]
{m : Multiset ι}
{f : ι → M}
[DecidableEq ι]
(i : ι)
(hf : ∀ (i' : ι), i' ≠ i → i' ∈ m → f i' = 1)
:
theorem
Multiset.sum_map_eq_nsmul_single
{ι : Type u_2}
{M : Type u_5}
[AddCommMonoid M]
{m : Multiset ι}
{f : ι → M}
[DecidableEq ι]
(i : ι)
(hf : ∀ (i' : ι), i' ≠ i → i' ∈ m → f i' = 0)
:
theorem
Multiset.prod_eq_pow_single
{M : Type u_5}
[CommMonoid M]
{s : Multiset M}
[DecidableEq M]
(a : M)
(h : ∀ (a' : M), a' ≠ a → a' ∈ s → a' = 1)
:
theorem
Multiset.sum_eq_nsmul_single
{M : Type u_5}
[AddCommMonoid M]
{s : Multiset M}
[DecidableEq M]
(a : M)
(h : ∀ (a' : M), a' ≠ a → a' ∈ s → a' = 0)
:
theorem
Multiset.sum_eq_zero
{M : Type u_5}
[AddCommMonoid M]
{s : Multiset M}
(h : ∀ x ∈ s, x = 0)
:
theorem
Multiset.prod_hom_ne_zero
{M : Type u_5}
{N : Type u_6}
[CommMonoid M]
[CommMonoid N]
{s : Multiset M}
(hs : s ≠ 0)
{F : Type u_8}
[FunLike F M N]
[MulHomClass F M N]
(f : F)
:
theorem
Multiset.sum_hom_ne_zero
{M : Type u_5}
{N : Type u_6}
[AddCommMonoid M]
[AddCommMonoid N]
{s : Multiset M}
(hs : s ≠ 0)
{F : Type u_8}
[FunLike F M N]
[AddHomClass F M N]
(f : F)
:
theorem
Multiset.prod_hom
{M : Type u_5}
{N : Type u_6}
[CommMonoid M]
[CommMonoid N]
(s : Multiset M)
{F : Type u_8}
[FunLike F M N]
[MonoidHomClass F M N]
(f : F)
:
theorem
Multiset.sum_hom
{M : Type u_5}
{N : Type u_6}
[AddCommMonoid M]
[AddCommMonoid N]
(s : Multiset M)
{F : Type u_8}
[FunLike F M N]
[AddMonoidHomClass F M N]
(f : F)
:
theorem
Multiset.prod_hom'
{ι : Type u_2}
{M : Type u_5}
{N : Type u_6}
[CommMonoid M]
[CommMonoid N]
(s : Multiset ι)
{F : Type u_8}
[FunLike F M N]
[MonoidHomClass F M N]
(f : F)
(g : ι → M)
:
theorem
Multiset.sum_hom'
{ι : Type u_2}
{M : Type u_5}
{N : Type u_6}
[AddCommMonoid M]
[AddCommMonoid N]
(s : Multiset ι)
{F : Type u_8}
[FunLike F M N]
[AddMonoidHomClass F M N]
(f : F)
(g : ι → M)
:
theorem
Multiset.prod_hom₂_ne_zero
{ι : Type u_2}
{M : Type u_5}
{N : Type u_6}
{O : Type u_7}
[CommMonoid M]
[CommMonoid N]
[CommMonoid O]
{s : Multiset ι}
(hs : s ≠ 0)
(f : M → N → O)
(hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d)
(f₁ : ι → M)
(f₂ : ι → N)
:
theorem
Multiset.sum_hom₂_ne_zero
{ι : Type u_2}
{M : Type u_5}
{N : Type u_6}
{O : Type u_7}
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid O]
{s : Multiset ι}
(hs : s ≠ 0)
(f : M → N → O)
(hf : ∀ (a b : M) (c d : N), f (a + b) (c + d) = f a c + f b d)
(f₁ : ι → M)
(f₂ : ι → N)
:
theorem
Multiset.prod_hom₂
{ι : Type u_2}
{M : Type u_5}
{N : Type u_6}
{O : Type u_7}
[CommMonoid M]
[CommMonoid N]
[CommMonoid O]
(s : Multiset ι)
(f : M → N → O)
(hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d)
(hf' : f 1 1 = 1)
(f₁ : ι → M)
(f₂ : ι → N)
:
theorem
Multiset.sum_hom₂
{ι : Type u_2}
{M : Type u_5}
{N : Type u_6}
{O : Type u_7}
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid O]
(s : Multiset ι)
(f : M → N → O)
(hf : ∀ (a b : M) (c d : N), f (a + b) (c + d) = f a c + f b d)
(hf' : f 0 0 = 0)
(f₁ : ι → M)
(f₂ : ι → N)
:
theorem
map_multiset_prod
{F : Type u_1}
{M : Type u_5}
{N : Type u_6}
[CommMonoid M]
[CommMonoid N]
[FunLike F M N]
[MonoidHomClass F M N]
(f : F)
(s : Multiset M)
:
theorem
map_multiset_sum
{F : Type u_1}
{M : Type u_5}
{N : Type u_6}
[AddCommMonoid M]
[AddCommMonoid N]
[FunLike F M N]
[AddMonoidHomClass F M N]
(f : F)
(s : Multiset M)
:
theorem
map_multiset_ne_zero_prod
{F : Type u_1}
{M : Type u_5}
{N : Type u_6}
[CommMonoid M]
[CommMonoid N]
[FunLike F M N]
[MulHomClass F M N]
(f : F)
{s : Multiset M}
(hs : s ≠ 0)
:
theorem
map_multiset_ne_zero_sum
{F : Type u_1}
{M : Type u_5}
{N : Type u_6}
[AddCommMonoid M]
[AddCommMonoid N]
[FunLike F M N]
[AddHomClass F M N]
(f : F)
{s : Multiset M}
(hs : s ≠ 0)
:
theorem
MonoidHom.map_multiset_prod
{M : Type u_5}
{N : Type u_6}
[CommMonoid M]
[CommMonoid N]
(f : M →* N)
(s : Multiset M)
:
theorem
AddMonoidHom.map_multiset_sum
{M : Type u_5}
{N : Type u_6}
[AddCommMonoid M]
[AddCommMonoid N]
(f : M →+ N)
(s : Multiset M)
:
theorem
MulHom.map_multiset_ne_zero_prod
{M : Type u_5}
{N : Type u_6}
[CommMonoid M]
[CommMonoid N]
(f : M →ₙ* N)
(s : Multiset M)
(hs : s ≠ 0)
:
theorem
AddHom.map_multiset_ne_zero_sum
{M : Type u_5}
{N : Type u_6}
[AddCommMonoid M]
[AddCommMonoid N]
(f : M →ₙ+ N)
(s : Multiset M)
(hs : s ≠ 0)
:
theorem
Multiset.fst_prod
{M : Type u_5}
{N : Type u_6}
[CommMonoid M]
[CommMonoid N]
(s : Multiset (M × N))
:
theorem
Multiset.fst_sum
{M : Type u_5}
{N : Type u_6}
[AddCommMonoid M]
[AddCommMonoid N]
(s : Multiset (M × N))
:
theorem
Multiset.snd_prod
{M : Type u_5}
{N : Type u_6}
[CommMonoid M]
[CommMonoid N]
(s : Multiset (M × N))
:
theorem
Multiset.snd_sum
{M : Type u_5}
{N : Type u_6}
[AddCommMonoid M]
[AddCommMonoid N]
(s : Multiset (M × N))
:
Multiset.sum
, the sum of the elements of a multiset, promoted to a morphism of
AddCommMonoid
s.
Equations
- Multiset.sumAddMonoidHom = { toFun := Multiset.sum, map_zero' := ⋯, map_add' := ⋯ }
Instances For
@[simp]
theorem
Multiset.sum_map_tsub
{ι : Type u_2}
{M : Type u_5}
[AddCommMonoid M]
[PartialOrder M]
[ExistsAddOfLE M]
[CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2]
[ContravariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2]
[Sub M]
[OrderedSub M]
(l : Multiset ι)
{f g : ι → M}
(hfg : ∀ x ∈ l, g x ≤ f x)
: