Modified from Mathlib.Data.DFinsupp.Basic
def
DFinsupp'.sum
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
{d : (i : ι) → β i}
[DecidableEq ι]
[(i : ι) → (x : β i) → Decidable (x ≠ d i)]
[AddCommMonoid γ]
(f : ι →₀' [β i, d i])
(g : (i : ι) → β i → γ)
:
γ
DFinsupp'.sum f g is the sum of g i (f i) over the support of f.
Equations
- f.sum g = ∑ i ∈ f.support, g i (f i)
Instances For
def
DFinsupp'.prod
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
{d : (i : ι) → β i}
[DecidableEq ι]
[(i : ι) → (x : β i) → Decidable (x ≠ d i)]
[CommMonoid γ]
(f : ι →₀' [β i, d i])
(g : (i : ι) → β i → γ)
:
γ
DFinsupp'.prod f g is the product of g i (f i) over the support of f.
Equations
- f.prod g = ∏ i ∈ f.support, g i (f i)
Instances For
@[simp]
theorem
map_dfinsupp'_sum
{ι : Type u}
{β : ι → Type v}
{d : (i : ι) → β i}
[DecidableEq ι]
{R : Type u_1}
{S : Type u_2}
{H : Type u_3}
[(i : ι) → (x : β i) → Decidable (x ≠ d i)]
[AddCommMonoid R]
[AddCommMonoid S]
[FunLike H R S]
[AddMonoidHomClass H R S]
(h : H)
(f : ι →₀' [β i, d i])
(g : (i : ι) → β i → R)
:
h (f.sum g) = f.sum fun (a : ι) (b : β a) => h (g a b)
@[simp]
theorem
map_dfinsupp'_prod
{ι : Type u}
{β : ι → Type v}
{d : (i : ι) → β i}
[DecidableEq ι]
{R : Type u_1}
{S : Type u_2}
{H : Type u_3}
[(i : ι) → (x : β i) → Decidable (x ≠ d i)]
[CommMonoid R]
[CommMonoid S]
[FunLike H R S]
[MonoidHomClass H R S]
(h : H)
(f : ι →₀' [β i, d i])
(g : (i : ι) → β i → R)
:
h (f.prod g) = f.prod fun (a : ι) (b : β a) => h (g a b)
theorem
DFinsupp'.sum_mapRange_index
{ι : Type u}
{γ : Type w}
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
{d₁ : (i : ι) → β₁ i}
{d₂ : (i : ι) → β₂ i}
[DecidableEq ι]
[(i : ι) → (x : β₁ i) → Decidable (x ≠ d₁ i)]
[(i : ι) → (x : β₂ i) → Decidable (x ≠ d₂ i)]
[AddCommMonoid γ]
{f : (i : ι) → β₁ i → β₂ i}
{hf : ∀ (i : ι), f i (d₁ i) = d₂ i}
{g : ι →₀' [β₁ i, d₁ i]}
{h : (i : ι) → β₂ i → γ}
(h0 : ∀ (i : ι), h i (d₂ i) = 0)
:
(DFinsupp'.mapRange f hf g).sum h = g.sum fun (i : ι) (b : β₁ i) => h i (f i b)
theorem
DFinsupp'.prod_mapRange_index
{ι : Type u}
{γ : Type w}
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
{d₁ : (i : ι) → β₁ i}
{d₂ : (i : ι) → β₂ i}
[DecidableEq ι]
[(i : ι) → (x : β₁ i) → Decidable (x ≠ d₁ i)]
[(i : ι) → (x : β₂ i) → Decidable (x ≠ d₂ i)]
[CommMonoid γ]
{f : (i : ι) → β₁ i → β₂ i}
{hf : ∀ (i : ι), f i (d₁ i) = d₂ i}
{g : ι →₀' [β₁ i, d₁ i]}
{h : (i : ι) → β₂ i → γ}
(h0 : ∀ (i : ι), h i (d₂ i) = 1)
:
(DFinsupp'.mapRange f hf g).prod h = g.prod fun (i : ι) (b : β₁ i) => h i (f i b)
theorem
DFinsupp'.sum_default_index
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
{d : (i : ι) → β i}
[DecidableEq ι]
[(i : ι) → (x : β i) → Decidable (x ≠ d i)]
[AddCommMonoid γ]
{h : (i : ι) → β i → γ}
:
default.sum h = 0
theorem
DFinsupp'.prod_default_index
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
{d : (i : ι) → β i}
[DecidableEq ι]
[(i : ι) → (x : β i) → Decidable (x ≠ d i)]
[CommMonoid γ]
{h : (i : ι) → β i → γ}
:
default.prod h = 1
theorem
DFinsupp'.sum_single_index
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
{d : (i : ι) → β i}
[DecidableEq ι]
[(i : ι) → (x : β i) → Decidable (x ≠ d i)]
[AddCommMonoid γ]
{i : ι}
{b : β i}
{h : (i : ι) → β i → γ}
(hd : h i (d i) = 0)
:
(DFinsupp'.single d i b).sum h = h i b
theorem
DFinsupp'.prod_single_index
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
{d : (i : ι) → β i}
[DecidableEq ι]
[(i : ι) → (x : β i) → Decidable (x ≠ d i)]
[CommMonoid γ]
{i : ι}
{b : β i}
{h : (i : ι) → β i → γ}
(hd : h i (d i) = 1)
:
(DFinsupp'.single d i b).prod h = h i b
theorem
DFinsupp'.sum_comm
{γ : Type w}
{ι₁ : Type u_3}
{ι₂ : Type u_4}
{β₁ : ι₁ → Type u_1}
{β₂ : ι₂ → Type u_2}
[DecidableEq ι₁]
[DecidableEq ι₂]
{d₁ : (i : ι₁) → β₁ i}
{d₂ : (i : ι₂) → β₂ i}
[(i : ι₁) → (x : β₁ i) → Decidable (x ≠ d₁ i)]
[(i : ι₂) → (x : β₂ i) → Decidable (x ≠ d₂ i)]
[AddCommMonoid γ]
(f₁ : ι₁ →₀' [β₁ i, d₁ i])
(f₂ : ι₂ →₀' [β₂ i, d₂ i])
(h : (i : ι₁) → β₁ i → (i : ι₂) → β₂ i → γ)
:
(f₁.sum fun (i₁ : ι₁) (x₁ : β₁ i₁) => f₂.sum fun (i₂ : ι₂) (x₂ : β₂ i₂) => h i₁ x₁ i₂ x₂) = f₂.sum fun (i₂ : ι₂) (x₂ : β₂ i₂) => f₁.sum fun (i₁ : ι₁) (x₁ : β₁ i₁) => h i₁ x₁ i₂ x₂
theorem
DFinsupp'.prod_comm
{γ : Type w}
{ι₁ : Type u_3}
{ι₂ : Type u_4}
{β₁ : ι₁ → Type u_1}
{β₂ : ι₂ → Type u_2}
[DecidableEq ι₁]
[DecidableEq ι₂]
{d₁ : (i : ι₁) → β₁ i}
{d₂ : (i : ι₂) → β₂ i}
[(i : ι₁) → (x : β₁ i) → Decidable (x ≠ d₁ i)]
[(i : ι₂) → (x : β₂ i) → Decidable (x ≠ d₂ i)]
[CommMonoid γ]
(f₁ : ι₁ →₀' [β₁ i, d₁ i])
(f₂ : ι₂ →₀' [β₂ i, d₂ i])
(h : (i : ι₁) → β₁ i → (i : ι₂) → β₂ i → γ)
:
(f₁.prod fun (i₁ : ι₁) (x₁ : β₁ i₁) => f₂.prod fun (i₂ : ι₂) (x₂ : β₂ i₂) => h i₁ x₁ i₂ x₂) = f₂.prod fun (i₂ : ι₂) (x₂ : β₂ i₂) => f₁.prod fun (i₁ : ι₁) (x₁ : β₁ i₁) => h i₁ x₁ i₂ x₂
@[simp]
theorem
DFinsupp'.sum_zero
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
{d : (i : ι) → β i}
[DecidableEq ι]
[(i : ι) → (x : β i) → Decidable (x ≠ d i)]
[AddCommMonoid γ]
{f : ι →₀' [β i, d i]}
:
(f.sum fun (x : ι) (x : β x) => 0) = 0
@[simp]
theorem
DFinsupp'.prod_one
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
{d : (i : ι) → β i}
[DecidableEq ι]
[(i : ι) → (x : β i) → Decidable (x ≠ d i)]
[CommMonoid γ]
{f : ι →₀' [β i, d i]}
:
(f.prod fun (x : ι) (x : β x) => 1) = 1
@[simp]
theorem
DFinsupp'.sum_add
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
{d : (i : ι) → β i}
[DecidableEq ι]
[(i : ι) → (x : β i) → Decidable (x ≠ d i)]
[AddCommMonoid γ]
{f : ι →₀' [β i, d i]}
{h₁ : (i : ι) → β i → γ}
{h₂ : (i : ι) → β i → γ}
:
@[simp]
theorem
DFinsupp'.prod_mul
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
{d : (i : ι) → β i}
[DecidableEq ι]
[(i : ι) → (x : β i) → Decidable (x ≠ d i)]
[CommMonoid γ]
{f : ι →₀' [β i, d i]}
{h₁ : (i : ι) → β i → γ}
{h₂ : (i : ι) → β i → γ}
:
@[simp]
theorem
DFinsupp'.sum_neg
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
{d : (i : ι) → β i}
[DecidableEq ι]
[(i : ι) → (x : β i) → Decidable (x ≠ d i)]
[AddCommGroup γ]
{f : ι →₀' [β i, d i]}
{h : (i : ι) → β i → γ}
:
theorem
DFinsupp'.sum_eq_zero
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
{d : (i : ι) → β i}
[DecidableEq ι]
[(i : ι) → (x : β i) → Decidable (x ≠ d i)]
[AddCommMonoid γ]
{f : ι →₀' [β i, d i]}
{h : (i : ι) → β i → γ}
(hyp : ∀ (i : ι), h i (f i) = 0)
:
f.sum h = 0
theorem
DFinsupp'.prod_eq_one
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
{d : (i : ι) → β i}
[DecidableEq ι]
[(i : ι) → (x : β i) → Decidable (x ≠ d i)]
[CommMonoid γ]
{f : ι →₀' [β i, d i]}
{h : (i : ι) → β i → γ}
(hyp : ∀ (i : ι), h i (f i) = 1)
:
f.prod h = 1
theorem
DFinsupp'.smul_sum
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
{d : (i : ι) → β i}
[DecidableEq ι]
{α : Type u_1}
[Monoid α]
[(i : ι) → (x : β i) → Decidable (x ≠ d i)]
[AddCommMonoid γ]
[DistribMulAction α γ]
{f : ι →₀' [β i, d i]}
{h : (i : ι) → β i → γ}
{c : α}
:
theorem
dfinsupp_sum_mem
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
{d : (i : ι) → β i}
[DecidableEq ι]
[(i : ι) → (x : β i) → Decidable (x ≠ d i)]
[AddCommMonoid γ]
{S : Type u_1}
[SetLike S γ]
[AddSubmonoidClass S γ]
(s : S)
(f : ι →₀' [β i, d i])
(g : (i : ι) → β i → γ)
(h : ∀ (c : ι), f c ≠ d c → g c (f c) ∈ s)
:
f.sum g ∈ s
theorem
dfinsupp_prod_mem
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
{d : (i : ι) → β i}
[DecidableEq ι]
[(i : ι) → (x : β i) → Decidable (x ≠ d i)]
[CommMonoid γ]
{S : Type u_1}
[SetLike S γ]
[SubmonoidClass S γ]
(s : S)
(f : ι →₀' [β i, d i])
(g : (i : ι) → β i → γ)
(h : ∀ (c : ι), f c ≠ d c → g c (f c) ∈ s)
:
f.prod g ∈ s
@[simp]
theorem
DFinsupp'.sum_eq_sum_fintype
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
{d : (i : ι) → β i}
[DecidableEq ι]
[Fintype ι]
[(i : ι) → (x : β i) → Decidable (x ≠ d i)]
[AddCommMonoid γ]
(v : ι →₀' [β i, d i])
{f : (i : ι) → β i → γ}
(hf : ∀ (i : ι), f i (d i) = 0)
:
v.sum f = ∑ i : ι, f i (DFinsupp'.equivFunOnFintype v i)
@[simp]
theorem
DFinsupp'.prod_eq_prod_fintype
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
{d : (i : ι) → β i}
[DecidableEq ι]
[Fintype ι]
[(i : ι) → (x : β i) → Decidable (x ≠ d i)]
[CommMonoid γ]
(v : ι →₀' [β i, d i])
{f : (i : ι) → β i → γ}
(hf : ∀ (i : ι), f i (d i) = 1)
:
v.prod f = ∏ i : ι, f i (DFinsupp'.equivFunOnFintype v i)
@[simp]
theorem
DFinsupp'.prod_eq_zero_iff
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
{d : (i : ι) → β i}
[DecidableEq ι]
[CommMonoidWithZero γ]
[Nontrivial γ]
[NoZeroDivisors γ]
[(i : ι) → DecidableEq (β i)]
{f : ι →₀' [β i, d i]}
{g : (i : ι) → β i → γ}
:
theorem
DFinsupp'.prod_ne_zero_iff
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
{d : (i : ι) → β i}
[DecidableEq ι]
[CommMonoidWithZero γ]
[Nontrivial γ]
[NoZeroDivisors γ]
[(i : ι) → DecidableEq (β i)]
{f : ι →₀' [β i, d i]}
{g : (i : ι) → β i → γ}
:
theorem
DFinsupp'.sum_subtypeDomain_index
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
{d : (i : ι) → β i}
[DecidableEq ι]
[(i : ι) → (x : β i) → Decidable (x ≠ d i)]
[AddCommMonoid γ]
{v : ι →₀' [β i, d i]}
{p : ι → Prop}
[DecidablePred p]
{h : (i : ι) → β i → γ}
(hp : ∀ x ∈ v.support, p x)
:
((DFinsupp'.subtypeDomain p v).sum fun (i : Subtype p) (b : β ↑i) => h (↑i) b) = v.sum h
theorem
DFinsupp'.prod_subtypeDomain_index
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
{d : (i : ι) → β i}
[DecidableEq ι]
[(i : ι) → (x : β i) → Decidable (x ≠ d i)]
[CommMonoid γ]
{v : ι →₀' [β i, d i]}
{p : ι → Prop}
[DecidablePred p]
{h : (i : ι) → β i → γ}
(hp : ∀ x ∈ v.support, p x)
:
((DFinsupp'.subtypeDomain p v).prod fun (i : Subtype p) (b : β ↑i) => h (↑i) b) = v.prod h
@[simp]
theorem
AddMonoidHom.coe_dfinsupp'_sum
{ι : Type u}
{β : ι → Type v}
{d : (i : ι) → β i}
[DecidableEq ι]
{R : Type u_1}
{S : Type u_2}
[(i : ι) → (x : β i) → Decidable (x ≠ d i)]
[AddMonoid R]
[AddCommMonoid S]
(f : ι →₀' [β i, d i])
(g : (i : ι) → β i → R →+ S)
:
⇑(f.sum g) = f.sum fun (a : ι) (b : β a) => ⇑(g a b)
@[simp]
theorem
MonoidHom.coe_dfinsupp'_prod
{ι : Type u}
{β : ι → Type v}
{d : (i : ι) → β i}
[DecidableEq ι]
{R : Type u_1}
{S : Type u_2}
[(i : ι) → (x : β i) → Decidable (x ≠ d i)]
[Monoid R]
[CommMonoid S]
(f : ι →₀' [β i, d i])
(g : (i : ι) → β i → R →* S)
:
⇑(f.prod g) = f.prod fun (a : ι) (b : β a) => ⇑(g a b)
theorem
AddMonoidHom.dfinsupp'_sum_apply
{ι : Type u}
{β : ι → Type v}
{d : (i : ι) → β i}
[DecidableEq ι]
{R : Type u_1}
{S : Type u_2}
[(i : ι) → (x : β i) → Decidable (x ≠ d i)]
[AddMonoid R]
[AddCommMonoid S]
(f : ι →₀' [β i, d i])
(g : (i : ι) → β i → R →+ S)
(r : R)
:
(f.sum g) r = f.sum fun (a : ι) (b : β a) => (g a b) r
theorem
MonoidHom.dfinsupp'_prod_apply
{ι : Type u}
{β : ι → Type v}
{d : (i : ι) → β i}
[DecidableEq ι]
{R : Type u_1}
{S : Type u_2}
[(i : ι) → (x : β i) → Decidable (x ≠ d i)]
[Monoid R]
[CommMonoid S]
(f : ι →₀' [β i, d i])
(g : (i : ι) → β i → R →* S)
(r : R)
:
(f.prod g) r = f.prod fun (a : ι) (b : β a) => (g a b) r