Congruence modulo natural and integer numbers for big operators

In this file we prove various versions of the following theorem: if f i ≡ g i [MOD n] for all i ∈ s, then ∏ i ∈ s, f i ≡ ∏ i ∈ s, g i [MOD n], and similarly for sums.

We prove it for lists, multisets, and finsets, as well as for natural and integer numbers.

theorem Nat.ModEq.listProd_map {α : Type u_1} {n : ℕ} {l : List α} {f g : α → ℕ} (h : ∀ x ∈ l, f x ≡ g x [MOD n]) : (List.map f l).prod ≡ (List.map g l).prod [MOD n]

theorem Nat.ModEq.listProd_map_one {α : Type u_1} {n : ℕ} {l : List α} {f : α → ℕ} (h : ∀ x ∈ l, f x ≡ 1 [MOD n]) : (List.map f l).prod ≡ 1 [MOD n]

theorem Nat.ModEq.listProd_one {n : ℕ} {l : List ℕ} (h : ∀ x ∈ l, x ≡ 1 [MOD n]) : l.prod ≡ 1 [MOD n]

theorem Nat.ModEq.listSum_map {α : Type u_1} {n : ℕ} {l : List α} {f g : α → ℕ} (h : ∀ x ∈ l, f x ≡ g x [MOD n]) : (List.map f l).sum ≡ (List.map g l).sum [MOD n]

theorem Nat.ModEq.listSum_map_zero {α : Type u_1} {n : ℕ} {l : List α} {f : α → ℕ} (h : ∀ x ∈ l, f x ≡ 0 [MOD n]) : (List.map f l).sum ≡ 0 [MOD n]

theorem Nat.ModEq.listSum_zero {n : ℕ} {l : List ℕ} (h : ∀ x ∈ l, x ≡ 0 [MOD n]) : l.sum ≡ 0 [MOD n]

theorem Nat.ModEq.multisetProd_map {α : Type u_1} {n : ℕ} {f g : α → ℕ} {s : Multiset α} (h : ∀ x ∈ s, f x ≡ g x [MOD n]) : (Multiset.map f s).prod ≡ (Multiset.map g s).prod [MOD n]

theorem Nat.ModEq.multisetProd_map_one {α : Type u_1} {n : ℕ} {f : α → ℕ} {s : Multiset α} (h : ∀ x ∈ s, f x ≡ 1 [MOD n]) : (Multiset.map f s).prod ≡ 1 [MOD n]

theorem Nat.ModEq.multisetProd_one {n : ℕ} {s : Multiset ℕ} (h : ∀ x ∈ s, x ≡ 1 [MOD n]) : s.prod ≡ 1 [MOD n]

theorem Nat.ModEq.multisetSum_map {α : Type u_1} {n : ℕ} {f g : α → ℕ} {s : Multiset α} (h : ∀ x ∈ s, f x ≡ g x [MOD n]) : (Multiset.map f s).sum ≡ (Multiset.map g s).sum [MOD n]

theorem Nat.ModEq.multisetSum_map_zero {α : Type u_1} {n : ℕ} {f : α → ℕ} {s : Multiset α} (h : ∀ x ∈ s, f x ≡ 0 [MOD n]) : (Multiset.map f s).sum ≡ 0 [MOD n]

theorem Nat.ModEq.multisetSum_zero {n : ℕ} {s : Multiset ℕ} (h : ∀ x ∈ s, x ≡ 0 [MOD n]) : s.sum ≡ 0 [MOD n]

theorem Nat.ModEq.prod {α : Type u_1} {n : ℕ} {f g : α → ℕ} {s : Finset α} (h : ∀ x ∈ s, f x ≡ g x [MOD n]) : ∏ x ∈ s, f x ≡ ∏ x ∈ s, g x [MOD n]

theorem Nat.ModEq.prod_one {α : Type u_1} {n : ℕ} {f : α → ℕ} {s : Finset α} (h : ∀ x ∈ s, f x ≡ 1 [MOD n]) : ∏ x ∈ s, f x ≡ 1 [MOD n]

theorem Nat.ModEq.sum {α : Type u_1} {n : ℕ} {f g : α → ℕ} {s : Finset α} (h : ∀ x ∈ s, f x ≡ g x [MOD n]) : ∑ x ∈ s, f x ≡ ∑ x ∈ s, g x [MOD n]

theorem Nat.ModEq.sum_zero {α : Type u_1} {n : ℕ} {f : α → ℕ} {s : Finset α} (h : ∀ x ∈ s, f x ≡ 0 [MOD n]) : ∑ x ∈ s, f x ≡ 0 [MOD n]

theorem Nat.prod_modEq_ite {α : Type u_1} {n : ℕ} {f : α → ℕ} [DecidableEq α] {s : Finset α} {a : α} (hf : ∀ x ∈ s, x ≠ a → f x ≡ 1 [MOD n]) : ∏ x ∈ s, f x ≡ if a ∈ s then f a else 1 [MOD n]

theorem Nat.prod_modEq_single {α : Type u_1} {n : ℕ} {f : α → ℕ} {s : Finset α} {a : α} (ha : a ∉ s → f a ≡ 1 [MOD n]) (hf : ∀ x ∈ s, x ≠ a → f x ≡ 1 [MOD n]) : ∏ x ∈ s, f x ≡ f a [MOD n]

theorem Nat.sum_modEq_ite {α : Type u_1} {n : ℕ} {f : α → ℕ} [DecidableEq α] {s : Finset α} {a : α} (hf : ∀ x ∈ s, x ≠ a → f x ≡ 0 [MOD n]) : ∑ x ∈ s, f x ≡ if a ∈ s then f a else 0 [MOD n]

theorem Nat.sum_modEq_single {α : Type u_1} {n : ℕ} {f : α → ℕ} {s : Finset α} {a : α} (ha : a ∉ s → f a ≡ 0 [MOD n]) (hf : ∀ x ∈ s, x ≠ a → f x ≡ 0 [MOD n]) : ∑ x ∈ s, f x ≡ f a [MOD n]

theorem Int.ModEq.listProd_map {α : Type u_1} {n : ℤ} {l : List α} {f g : α → ℤ} (h : ∀ x ∈ l, f x ≡ g x [ZMOD n]) : (List.map f l).prod ≡ (List.map g l).prod [ZMOD n]

theorem Int.ModEq.listProd_map_one {α : Type u_1} {n : ℤ} {l : List α} {f : α → ℤ} (h : ∀ x ∈ l, f x ≡ 1 [ZMOD n]) : (List.map f l).prod ≡ 1 [ZMOD n]

theorem Int.ModEq.listProd_one {n : ℤ} {l : List ℤ} (h : ∀ x ∈ l, x ≡ 1 [ZMOD n]) : l.prod ≡ 1 [ZMOD n]

theorem Int.ModEq.listSum_map {α : Type u_1} {n : ℤ} {l : List α} {f g : α → ℤ} (h : ∀ x ∈ l, f x ≡ g x [ZMOD n]) : (List.map f l).sum ≡ (List.map g l).sum [ZMOD n]

theorem Int.ModEq.listSum_map_zero {α : Type u_1} {n : ℤ} {l : List α} {f : α → ℤ} (h : ∀ x ∈ l, f x ≡ 0 [ZMOD n]) : (List.map f l).sum ≡ 0 [ZMOD n]

theorem Int.ModEq.listSum_zero {n : ℤ} {l : List ℤ} (h : ∀ x ∈ l, x ≡ 0 [ZMOD n]) : l.sum ≡ 0 [ZMOD n]

theorem Int.ModEq.multisetProd_map {α : Type u_1} {n : ℤ} {f g : α → ℤ} {s : Multiset α} (h : ∀ x ∈ s, f x ≡ g x [ZMOD n]) : (Multiset.map f s).prod ≡ (Multiset.map g s).prod [ZMOD n]

theorem Int.ModEq.multisetProd_map_one {α : Type u_1} {n : ℤ} {f : α → ℤ} {s : Multiset α} (h : ∀ x ∈ s, f x ≡ 1 [ZMOD n]) : (Multiset.map f s).prod ≡ 1 [ZMOD n]

theorem Int.ModEq.multisetProd_one {n : ℤ} {s : Multiset ℤ} (h : ∀ x ∈ s, x ≡ 1 [ZMOD n]) : s.prod ≡ 1 [ZMOD n]

theorem Int.ModEq.multisetSum_map {α : Type u_1} {n : ℤ} {f g : α → ℤ} {s : Multiset α} (h : ∀ x ∈ s, f x ≡ g x [ZMOD n]) : (Multiset.map f s).sum ≡ (Multiset.map g s).sum [ZMOD n]

theorem Int.ModEq.multisetSum_map_zero {α : Type u_1} {n : ℤ} {f : α → ℤ} {s : Multiset α} (h : ∀ x ∈ s, f x ≡ 0 [ZMOD n]) : (Multiset.map f s).sum ≡ 0 [ZMOD n]

theorem Int.ModEq.multisetSum_zero {n : ℤ} {s : Multiset ℤ} (h : ∀ x ∈ s, x ≡ 0 [ZMOD n]) : s.sum ≡ 0 [ZMOD n]

theorem Int.ModEq.prod {α : Type u_1} {n : ℤ} {f g : α → ℤ} {s : Finset α} (h : ∀ x ∈ s, f x ≡ g x [ZMOD n]) : ∏ x ∈ s, f x ≡ ∏ x ∈ s, g x [ZMOD n]

theorem Int.ModEq.prod_one {α : Type u_1} {n : ℤ} {f : α → ℤ} {s : Finset α} (h : ∀ x ∈ s, f x ≡ 1 [ZMOD n]) : ∏ x ∈ s, f x ≡ 1 [ZMOD n]

theorem Int.ModEq.sum {α : Type u_1} {n : ℤ} {f g : α → ℤ} {s : Finset α} (h : ∀ x ∈ s, f x ≡ g x [ZMOD n]) : ∑ x ∈ s, f x ≡ ∑ x ∈ s, g x [ZMOD n]

theorem Int.ModEq.sum_zero {α : Type u_1} {n : ℤ} {f : α → ℤ} {s : Finset α} (h : ∀ x ∈ s, f x ≡ 0 [ZMOD n]) : ∑ x ∈ s, f x ≡ 0 [ZMOD n]

theorem Int.prod_modEq_ite {α : Type u_1} {n : ℤ} {f : α → ℤ} [DecidableEq α] {s : Finset α} {a : α} (hf : ∀ x ∈ s, x ≠ a → f x ≡ 1 [ZMOD n]) : ∏ x ∈ s, f x ≡ if a ∈ s then f a else 1 [ZMOD n]

theorem Int.prod_modEq_single {α : Type u_1} {n : ℤ} {f : α → ℤ} {s : Finset α} {a : α} (ha : a ∉ s → f a ≡ 1 [ZMOD n]) (hf : ∀ x ∈ s, x ≠ a → f x ≡ 1 [ZMOD n]) : ∏ x ∈ s, f x ≡ f a [ZMOD n]

theorem Int.sum_modEq_ite {α : Type u_1} {n : ℤ} {f : α → ℤ} [DecidableEq α] {s : Finset α} {a : α} (hf : ∀ x ∈ s, x ≠ a → f x ≡ 0 [ZMOD n]) : ∑ x ∈ s, f x ≡ if a ∈ s then f a else 0 [ZMOD n]

theorem Int.sum_modEq_single {α : Type u_1} {n : ℤ} {f : α → ℤ} {s : Finset α} {a : α} (ha : a ∉ s → f a ≡ 0 [ZMOD n]) (hf : ∀ x ∈ s, x ≠ a → f x ≡ 0 [ZMOD n]) : ∑ x ∈ s, f x ≡ f a [ZMOD n]