Algorithm.Algebra.BigOperators.DFinsupp'

Modified from Mathlib.Data.DFinsupp.Basic

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

source

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

source

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

source

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

source

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) :

(mapRange f hf g).prod h = g.prod fun (i : ι) (b : β₁ i) => h i (f i b)

source

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) :

(mapRange f hf g).sum h = g.sum fun (i : ι) (b : β₁ i) => h i (f i b)

source

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

source

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

source

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) :

(single d i b).prod h = h i b

source

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) :

(single d i b).sum h = h i b

source

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₂

source

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₂

source

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

source

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

source

@[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₁ h₂ : (i : ι) → β i → γ} :

(f.prod fun (i : ι) (b : β i) => h₁ i b * h₂ i b) = f.prod h₁ * f.prod h₂

source

@[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₁ h₂ : (i : ι) → β i → γ} :

(f.sum fun (i : ι) (b : β i) => h₁ i b + h₂ i b) = f.sum h₁ + f.sum h₂

source

@[simp]

theorem DFinsupp'.prod_inv {ι : Type u} {γ : Type w} {β : ι → Type v} {d : (i : ι) → β i} [DecidableEq ι] [(i : ι) → (x : β i) → Decidable (x ≠ d i)] [CommGroup γ] {f : ι →₀' [β i, d i]} {h : (i : ι) → β i → γ} :

(f.prod fun (i : ι) (b : β i) => (h i b)⁻¹) = (f.prod h)⁻¹

source

@[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 → γ} :

(f.sum fun (i : ι) (b : β i) => -h i b) = -f.sum h

source

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

source

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

source

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 : α} :

c • f.sum h = f.sum fun (a : ι) (b : β a) => c • h a b

source

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

source

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

source

@[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 (equivFunOnFintype v i)

source

@[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 (equivFunOnFintype v i)

source

@[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 → γ} :

f.prod g = 0 ↔ ∃ i ∈ f.support, g i (f i) = 0

source

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 → γ} :

f.prod g ≠ 0 ↔ ∀ i ∈ f.support, g i (f i) ≠ 0

source

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) :

((subtypeDomain p v).prod fun (i : Subtype p) (b : β ↑i) => h (↑i) b) = v.prod h

source

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) :

((subtypeDomain p v).sum fun (i : Subtype p) (b : β ↑i) => h (↑i) b) = v.sum h

source

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

source

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

source

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

source

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