Interactions between ∑, ∏ and RingCon

TODO: some of the typeclass assumptions in this file can be weakened if more instances are added for RingCon.Quotient.

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.

@[simp]

theorem RingCon.coe_listProd {ι : Type u_1} {S : Type u_2} [Add S] [Monoid S] (t : RingCon S) (l : List ι) (f : ι → S) : ↑(List.map f l).prod = (List.map (fun (i : ι) => ↑(f i)) l).prod

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.

@[simp]

theorem RingCon.coe_listSum {ι : Type u_1} {S : Type u_2} [AddMonoid S] [Mul S] (t : RingCon S) (l : List ι) (f : ι → S) : ↑(List.map f l).sum = (List.map (fun (i : ι) => ↑(f i)) l).sum

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.

@[simp]

theorem RingCon.coe_multisetProd {ι : Type u_1} {S : Type u_2} [Add S] [CommMonoid S] (t : RingCon S) (s : Multiset ι) (f : ι → S) : ↑(Multiset.map f s).prod = (Multiset.map (fun (i : ι) => ↑(f i)) s).prod

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.

@[simp]

theorem RingCon.coe_multisetSum {ι : Type u_1} {S : Type u_2} [AddCommMonoid S] [Mul S] (t : RingCon S) (s : Multiset ι) (f : ι → S) : ↑(Multiset.map f s).sum = (Multiset.map (fun (i : ι) => ↑(f i)) s).sum

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.

@[simp]

theorem RingCon.coe_finsetProd {ι : Type u_1} {S : Type u_2} [Add S] [CommMonoid S] (t : RingCon S) (s : Finset ι) (f : ι → S) : ↑(s.prod f) = ∏ i ∈ s, ↑(f i)

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.

@[simp]

theorem RingCon.coe_finsetSum {ι : Type u_1} {S : Type u_2} [AddCommMonoid S] [Mul S] (t : RingCon S) (s : Finset ι) (f : ι → S) : ↑(s.sum f) = ∑ i ∈ s, ↑(f i)

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

@[simp]

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

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

@[simp]

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

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

@[simp]

theorem RingCon.coe_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 : (i : ι) → β i → M) (f : Π₀ (i : ι), β i) : ↑(f.prod h) = f.prod fun (i : ι) (b : β i) => ↑(h i b)

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

@[simp]

theorem RingCon.coe_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 : (i : ι) → β i → M) (f : Π₀ (i : ι), β i) : ↑(f.sum h) = f.sum fun (i : ι) (b : β i) => ↑(h i b)

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)

@[simp]

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