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.

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.

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.

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

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

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)

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