feat(algebra/big_operators/basic): finset.sum under mod (#18364)

and `∏ a in s, f a = b ^ s.card` if `f a = b` for all `a`

src/algebra/big_operators/basic.lean

@@ -1131,6 +1131,10 @@ end
 @[simp, to_additive] lemma prod_const (b : β) : (∏ x in s, b) = b ^ s.card :=
 (congr_arg _ $ s.val.map_const b).trans $ multiset.prod_replicate s.card b
 
+@[to_additive sum_eq_card_nsmul] lemma prod_eq_pow_card {b : β} (hf : ∀ a ∈ s, f a = b) :
+  ∏ a in s, f a = b ^ s.card :=
+(prod_congr rfl hf).trans $ prod_const _
+
 @[to_additive]
 lemma pow_eq_prod_const (b : β) : ∀ n, b ^ n = ∏ k in range n, b := by simp
 
@@ -1570,6 +1574,22 @@ lemma prod_unique_nonempty {α β : Type*} [comm_monoid β] [unique α]
   (∏ x in s, f x) = f default :=
 by rw [h.eq_singleton_default, finset.prod_singleton]
 
+lemma sum_nat_mod (s : finset α) (n : ℕ) (f : α → ℕ) :
+  (∑ i in s, f i) % n = (∑ i in s, f i % n) % n :=
+(multiset.sum_nat_mod _ _).trans $ by rw [finset.sum, multiset.map_map]
+
+lemma prod_nat_mod (s : finset α) (n : ℕ) (f : α → ℕ) :
+  (∏ i in s, f i) % n = (∏ i in s, f i % n) % n :=
+(multiset.prod_nat_mod _ _).trans $ by rw [finset.prod, multiset.map_map]
+
+lemma sum_int_mod (s : finset α) (n : ℤ) (f : α → ℤ) :
+  (∑ i in s, f i) % n = (∑ i in s, f i % n) % n :=
+(multiset.sum_int_mod _ _).trans $ by rw [finset.sum, multiset.map_map]
+
+lemma prod_int_mod (s : finset α) (n : ℤ) (f : α → ℤ) :
+  (∏ i in s, f i) % n = (∏ i in s, f i % n) % n :=
+(multiset.prod_int_mod _ _).trans $ by rw [finset.prod, multiset.map_map]
+
 end finset
 
 namespace fintype

src/algebra/big_operators/multiset/basic.lean

@@ -418,6 +418,18 @@ lemma abs_sum_le_sum_abs [linear_ordered_add_comm_group α] {s : multiset α} :
   abs s.sum ≤ (s.map abs).sum :=
 le_sum_of_subadditive _ abs_zero abs_add s
 
+lemma sum_nat_mod (s : multiset ℕ) (n : ℕ) : s.sum % n = (s.map (% n)).sum % n :=
+by induction s using multiset.induction; simp [nat.add_mod, *]
+
+lemma prod_nat_mod (s : multiset ℕ) (n : ℕ) : s.prod % n = (s.map (% n)).prod % n :=
+by induction s using multiset.induction; simp [nat.mul_mod, *]
+
+lemma sum_int_mod (s : multiset ℤ) (n : ℤ) : s.sum % n = (s.map (% n)).sum % n :=
+by induction s using multiset.induction; simp [int.add_mod, *]
+
+lemma prod_int_mod (s : multiset ℤ) (n : ℤ) : s.prod % n = (s.map (% n)).prod % n :=
+by induction s using multiset.induction; simp [int.mul_mod, *]
+
 end multiset
 
 @[to_additive]

src/data/list/big_operators/basic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Floris van Doorn, Sébastien Gouëzel, Alex J. Best
 -/
+import data.int.order.basic
 import data.list.forall2
 
 /-!
@@ -543,6 +544,18 @@ by rw [div_eq_mul_inv, alternating_prod_cons']
 
 end alternating
 
+lemma sum_nat_mod (l : list ℕ) (n : ℕ) : l.sum % n = (l.map (% n)).sum % n :=
+by induction l; simp [nat.add_mod, *]
+
+lemma prod_nat_mod (l : list ℕ) (n : ℕ) : l.prod % n = (l.map (% n)).prod % n :=
+by induction l; simp [nat.mul_mod, *]
+
+lemma sum_int_mod (l : list ℤ) (n : ℤ) : l.sum % n = (l.map (% n)).sum % n :=
+by induction l; simp [int.add_mod, *]
+
+lemma prod_int_mod (l : list ℤ) (n : ℤ) : l.prod % n = (l.map (% n)).prod % n :=
+by induction l; simp [int.mul_mod, *]
+
 end list
 
 section monoid_hom