Interactions between ∑, ∏ and RingCon

theorem RingCon.listSum {ι : Type u_1} {S : Type u_2} [AddMonoid S] [Mul S] (t : RingCon S) (l : List ι) {f : ι → S} {g : ι → S} (h : ∀ i ∈ l, t (f i) (g i)) : t (List.map f l).sum (List.map g l).sum

Congruence relation of a ring preserves finite sum indexed by a list.

theorem RingCon.multisetSum {ι : Type u_1} {S : Type u_2} [AddCommMonoid S] [Mul S] (t : RingCon S) (s : Multiset ι) {f : ι → S} {g : ι → S} (h : ∀ i ∈ s, t (f i) (g i)) : t (Multiset.map f s).sum (Multiset.map g s).sum

Congruence relation of a ring preserves finite sum indexed by a multiset.

theorem RingCon.finsetSum {ι : Type u_1} {S : Type u_2} [AddCommMonoid S] [Mul S] (t : RingCon S) (s : Finset ι) {f : ι → S} {g : ι → S} (h : ∀ i ∈ s, t (f i) (g i)) : t (s.sum f) (s.sum g)

Congruence relation of a ring preserves finite sum.