Interactions between ∑, ∏ and (Add)Con

theorem AddCon.list_sum {ι : Type u_1} {M : Type u_2} [AddMonoid M] (c : AddCon M) {l : List ι} {f : ι → M} {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.list_prod {ι : Type u_1} {M : Type u_2} [Monoid M] (c : Con M) {l : List ι} {f : ι → M} {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.multiset_sum {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] (c : AddCon M) {s : Multiset ι} {f : ι → M} {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.multiset_prod {ι : Type u_1} {M : Type u_2} [CommMonoid M] (c : Con M) {s : Multiset ι} {f : ι → M} {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.finset_sum {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] (c : AddCon M) (s : Finset ι) {f : ι → M} {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.finset_prod {ι : Type u_1} {M : Type u_2} [CommMonoid M] (c : Con M) (s : Finset ι) {f : ι → M} {g : ι → M} (h : ∀ i ∈ s, c (f i) (g i)) : c (s.prod f) (s.prod g)

Multiplicative congruence relations preserve finite product.