Interactions between ∑, ∏ and RingCon

theorem RingCon.listProd {ι : Type u_1} {S : Type u_2} [Add S] [Monoid S] (t : RingCon S) (l : List ι) {f g : ι → S} (h : ∀ i ∈ l, t (f i) (g i)) : t (List.map f l).prod (List.map g l).prod

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

theorem RingCon.listSum {ι : Type u_1} {S : Type u_2} [AddMonoid S] [Mul S] (t : RingCon S) (l : List ι) {f 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.multisetProd {ι : Type u_1} {S : Type u_2} [Add S] [CommMonoid S] (t : RingCon S) (s : Multiset ι) {f g : ι → S} (h : ∀ i ∈ s, t (f i) (g i)) : t (Multiset.map f s).prod (Multiset.map g s).prod

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

theorem RingCon.multisetSum {ι : Type u_1} {S : Type u_2} [AddCommMonoid S] [Mul S] (t : RingCon S) (s : Multiset ι) {f 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.finsetProd {ι : Type u_1} {S : Type u_2} [Add S] [CommMonoid S] (t : RingCon S) (s : Finset ι) {f g : ι → S} (h : ∀ i ∈ s, t (f i) (g i)) : t (s.prod f) (s.prod g)

Congruence relation of a ring preserves finite product.

theorem RingCon.finsetSum {ι : Type u_1} {S : Type u_2} [AddCommMonoid S] [Mul S] (t : RingCon S) (s : Finset ι) {f 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.

theorem RingCon.finsuppProd {ι : Type u_1} {β : Type u_2} {M : Type u_3} [Add M] [CommMonoid M] [Zero β] (c : RingCon 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 RingCon.finsuppSum {ι : Type u_1} {β : Type u_2} {M : Type u_3} [AddCommMonoid M] [Mul M] [Zero β] (c : RingCon 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 RingCon.dfinsuppProd {ι : Type u_1} {β : ι → Type u_2} {M : Type u_3} [DecidableEq ι] [Add M] [CommMonoid M] [(i : ι) → Zero (β i)] [(i : ι) → (y : β i) → Decidable (y ≠ 0)] (c : RingCon 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 RingCon.dfinsuppSum {ι : Type u_1} {β : ι → Type u_2} {M : Type u_3} [DecidableEq ι] [AddCommMonoid M] [Mul M] [(i : ι) → Zero (β i)] [(i : ι) → (y : β i) → Decidable (y ≠ 0)] (c : RingCon 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 RingCon.dfinsuppSumAddHom {ι : Type u_1} {β : ι → Type u_2} {M : Type u_3} [DecidableEq ι] [AddCommMonoid M] [Mul M] [(i : ι) → AddCommMonoid (β i)] (c : RingCon 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)