Interactions between ∑, ∏ and (Add)Con

theorem Con.list_prod {ι : Type u_1} {M : Type u_2} [MulOneClass M] (c : Con M) {l : List ι} {f g : ι → M} (h : ∀ x ∈ l, c (f x) (g x)) : c (List.map f l).prod (List.map g l).prod

Multiplicative congruence relations preserve product indexed by a list.

theorem AddCon.list_sum {ι : Type u_1} {M : Type u_2} [AddZeroClass M] (c : AddCon M) {l : List ι} {f g : ι → M} (h : ∀ x ∈ l, c (f x) (g x)) : c (List.map f l).sum (List.map g l).sum

Additive congruence relations preserve sum indexed by a list.

@[simp]

theorem Con.coe_listProd {ι : Type u_1} {M : Type u_2} [MulOneClass M] (c : Con M) (l : List ι) (f : ι → M) : ↑(List.map f l).prod = (List.map (fun (i : ι) => ↑(f i)) l).prod

@[simp]

theorem AddCon.coe_listSum {ι : Type u_1} {M : Type u_2} [AddZeroClass M] (c : AddCon M) (l : List ι) (f : ι → M) : ↑(List.map f l).sum = (List.map (fun (i : ι) => ↑(f i)) l).sum

theorem Con.multiset_prod {ι : Type u_1} {M : Type u_2} [CommMonoid M] (c : Con M) {s : Multiset ι} {f g : ι → M} (h : ∀ x ∈ s, c (f x) (g x)) : c (Multiset.map f s).prod (Multiset.map g s).prod

Multiplicative congruence relations preserve product indexed by a multiset.

theorem AddCon.multiset_sum {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] (c : AddCon M) {s : Multiset ι} {f g : ι → M} (h : ∀ x ∈ s, c (f x) (g x)) : c (Multiset.map f s).sum (Multiset.map g s).sum

Additive congruence relations preserve sum indexed by a multiset.

@[simp]

theorem Con.coe_multisetProd {ι : Type u_1} {M : Type u_2} [CommMonoid M] (c : Con M) (s : Multiset ι) (f : ι → M) : ↑(Multiset.map f s).prod = (Multiset.map (fun (i : ι) => ↑(f i)) s).prod

@[simp]

theorem AddCon.coe_multisetSum {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] (c : AddCon M) (s : Multiset ι) (f : ι → M) : ↑(Multiset.map f s).sum = (Multiset.map (fun (i : ι) => ↑(f i)) s).sum

theorem Con.finsetProd {ι : Type u_1} {M : Type u_2} [CommMonoid M] (c : Con M) (s : Finset ι) {f g : ι → M} (h : ∀ i ∈ s, c (f i) (g i)) : c (s.prod f) (s.prod g)

Multiplicative congruence relations preserve finite product.

theorem AddCon.finsetSum {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] (c : AddCon M) (s : Finset ι) {f g : ι → M} (h : ∀ i ∈ s, c (f i) (g i)) : c (s.sum f) (s.sum g)

Additive congruence relations preserve finite sum.

@[simp]

theorem Con.coe_finsetProd {ι : Type u_1} {M : Type u_2} [CommMonoid M] (c : Con M) (s : Finset ι) (f : ι → M) : ↑(s.prod f) = ∏ i ∈ s, ↑(f i)

@[simp]

theorem AddCon.coe_finsetSum {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] (c : AddCon M) (s : Finset ι) (f : ι → M) : ↑(s.sum f) = ∑ i ∈ s, ↑(f i)

theorem Con.finsuppProd {ι : Type u_1} {β : Type u_2} {M : Type u_3} [CommMonoid M] [Zero β] (c : Con M) (h h' : ι → β → M) {f g : ι →₀ β} (hf : ∀ (i : ι), c (h i 0) 1) (hf' : ∀ (i : ι), c (h' i 0) 1) (H : ∀ (i : ι), c (h i (f i)) (h' i (g i))) : c (f.prod h) (g.prod h')

theorem AddCon.finsuppSum {ι : Type u_1} {β : Type u_2} {M : Type u_3} [AddCommMonoid M] [Zero β] (c : AddCon M) (h h' : ι → β → M) {f g : ι →₀ β} (hf : ∀ (i : ι), c (h i 0) 0) (hf' : ∀ (i : ι), c (h' i 0) 0) (H : ∀ (i : ι), c (h i (f i)) (h' i (g i))) : c (f.sum h) (g.sum h')

@[simp]

theorem Con.coe_finsuppProd {ι : Type u_1} {β : Type u_2} {M : Type u_3} [CommMonoid M] [Zero β] (c : Con M) (h : ι → β → M) (f : ι →₀ β) : ↑(f.prod h) = f.prod fun (i : ι) (b : β) => ↑(h i b)

@[simp]

theorem AddCon.coe_finsuppSum {ι : Type u_1} {β : Type u_2} {M : Type u_3} [AddCommMonoid M] [Zero β] (c : AddCon M) (h : ι → β → M) (f : ι →₀ β) : ↑(f.sum h) = f.sum fun (i : ι) (b : β) => ↑(h i b)

theorem Con.dfinsuppProd {ι : Type u_1} {β : ι → Type u_2} {M : Type u_3} [DecidableEq ι] [CommMonoid M] [(i : ι) → Zero (β i)] [(i : ι) → (y : β i) → Decidable (y ≠ 0)] (c : Con M) (h h' : (i : ι) → β i → M) {f g : Π₀ (i : ι), β i} (hf : ∀ (i : ι), c (h i 0) 1) (hf' : ∀ (i : ι), c (h' i 0) 1) (H : ∀ (i : ι), c (h i (f i)) (h' i (g i))) : c (f.prod h) (g.prod h')

theorem AddCon.dfinsuppSum {ι : Type u_1} {β : ι → Type u_2} {M : Type u_3} [DecidableEq ι] [AddCommMonoid M] [(i : ι) → Zero (β i)] [(i : ι) → (y : β i) → Decidable (y ≠ 0)] (c : AddCon M) (h h' : (i : ι) → β i → M) {f g : Π₀ (i : ι), β i} (hf : ∀ (i : ι), c (h i 0) 0) (hf' : ∀ (i : ι), c (h' i 0) 0) (H : ∀ (i : ι), c (h i (f i)) (h' i (g i))) : c (f.sum h) (g.sum h')

@[simp]

theorem Con.coe_dfinsuppProd {ι : Type u_1} {β : ι → Type u_2} {M : Type u_3} [DecidableEq ι] [CommMonoid M] [(i : ι) → Zero (β i)] [(i : ι) → (y : β i) → Decidable (y ≠ 0)] (c : Con M) (h : (i : ι) → β i → M) (f : Π₀ (i : ι), β i) : ↑(f.prod h) = f.prod fun (i : ι) (b : β i) => ↑(h i b)

@[simp]

theorem AddCon.coe_dfinsuppSum {ι : Type u_1} {β : ι → Type u_2} {M : Type u_3} [DecidableEq ι] [AddCommMonoid M] [(i : ι) → Zero (β i)] [(i : ι) → (y : β i) → Decidable (y ≠ 0)] (c : AddCon M) (h : (i : ι) → β i → M) (f : Π₀ (i : ι), β i) : ↑(f.sum h) = f.sum fun (i : ι) (b : β i) => ↑(h i b)

theorem AddCon.dfinsuppSumAddHom {ι : Type u_1} {β : ι → Type u_2} {M : Type u_3} [DecidableEq ι] [AddCommMonoid M] [(i : ι) → AddCommMonoid (β i)] (c : AddCon M) (h h' : (i : ι) → β i →+ M) {f g : Π₀ (i : ι), β i} (H : ∀ (i : ι), c ((h i) (f i)) ((h' i) (g i))) : c ((DFinsupp.sumAddHom h) f) ((DFinsupp.sumAddHom h') g)

@[simp]

theorem AddCon.coe_dfinsuppSumAddHom {ι : Type u_1} {β : ι → Type u_2} {M : Type u_3} [DecidableEq ι] [AddCommMonoid M] [(i : ι) → AddCommMonoid (β i)] (c : AddCon M) (h : (i : ι) → β i →+ M) (f : Π₀ (i : ι), β i) : ↑((DFinsupp.sumAddHom h) f) = (DFinsupp.sumAddHom fun (i : ι) => c.mk'.comp (h i)) f

@[deprecated AddCon.finsetSum (since := "2026-04-08")]

theorem AddCon.finset_sum {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] (c : AddCon M) (s : Finset ι) {f g : ι → M} (h : ∀ i ∈ s, c (f i) (g i)) : c (s.sum f) (s.sum g)

Alias of AddCon.finsetSum.

---

Additive congruence relations preserve finite sum.

@[deprecated Con.finsetProd (since := "2026-04-08")]

theorem Con.finset_prod {ι : Type u_1} {M : Type u_2} [CommMonoid M] (c : Con M) (s : Finset ι) {f g : ι → M} (h : ∀ i ∈ s, c (f i) (g i)) : c (s.prod f) (s.prod g)

Alias of Con.finsetProd.

---

Multiplicative congruence relations preserve finite product.