feat: add some lemmas about Finsupp.indicator (#2258)

mathlib3 PR: leanprover-community/mathlib#17413



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib/Algebra/BigOperators/Finsupp.lean

@@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 
 ! This file was ported from Lean 3 source module algebra.big_operators.finsupp
-! leanprover-community/mathlib commit f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
+! leanprover-community/mathlib commit 842328d9df7e96fd90fc424e115679c15fb23a71
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
-import Mathlib.Data.Finsupp.Defs
+import Mathlib.Data.Finsupp.Indicator
 import Mathlib.Algebra.BigOperators.Pi
 import Mathlib.Algebra.BigOperators.Ring
 import Mathlib.Algebra.BigOperators.Order
@@ -602,6 +602,25 @@ theorem prod_dvd_prod_of_subset_of_dvd [AddCommMonoid M] [CommMonoid N] {f1 f2 :
     exact h2
 #align finsupp.prod_dvd_prod_of_subset_of_dvd Finsupp.prod_dvd_prod_of_subset_of_dvd
 
+lemma indicator_eq_sum_single [AddCommMonoid M] (s : Finset α) (f : ∀ a ∈ s, M) :
+    indicator s f = ∑ x in s.attach, single ↑x (f x x.2) := by
+  rw [← sum_single (indicator s f), sum, sum_subset (support_indicator_subset _ _), ← sum_attach]
+  · refine' Finset.sum_congr rfl (fun _ _ => _)
+    rw [indicator_of_mem]
+  · intro i _ hi
+    rw [not_mem_support_iff.mp hi, single_zero]
+#align finsupp.indicator_eq_sum_single Finsupp.indicator_eq_sum_single
+
+@[to_additive (attr := simp)]
+lemma prod_indicator_index [Zero M] [CommMonoid N]
+    {s : Finset α} (f : ∀ a ∈ s, M) {h : α → M → N} (h_zero : ∀ a ∈ s, h a 0 = 1) :
+    (indicator s f).prod h = ∏ x in s.attach, h ↑x (f x x.2) := by
+  rw [prod_of_support_subset _ (support_indicator_subset _ _) h h_zero, ← prod_attach]
+  refine' Finset.prod_congr rfl (fun _ _ => _)
+  rw [indicator_of_mem]
+#align finsupp.prod_indicator_index Finsupp.prod_indicator_index
+#align finsupp.sum_indicator_index Finsupp.sum_indicator_index
+
 end Finsupp
 
 theorem Finset.sum_apply' : (∑ k in s, f k) i = ∑ k in s, f k i :=

Mathlib/Data/Finsupp/Defs.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Scott Morrison
 
 ! This file was ported from Lean 3 source module data.finsupp.defs
-! leanprover-community/mathlib commit 6623e6af705e97002a9054c1c05a980180276fc1
+! leanprover-community/mathlib commit 842328d9df7e96fd90fc424e115679c15fb23a71
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -317,11 +317,11 @@ theorem single_apply_left {f : α → β} (hf : Function.Injective f) (x z : α)
     single (f x) y (f z) = single x y z := by classical simp only [single_apply, hf.eq_iff]
 #align finsupp.single_apply_left Finsupp.single_apply_left
 
-theorem single_eq_indicator : ⇑(single a b) = Set.indicator {a} fun _ => b := by
+theorem single_eq_set_indicator : ⇑(single a b) = Set.indicator {a} fun _ => b := by
   classical
   ext
   simp [single_apply, Set.indicator, @eq_comm _ a]
-#align finsupp.single_eq_indicator Finsupp.single_eq_indicator
+#align finsupp.single_eq_set_indicator Finsupp.single_eq_set_indicator
 
 @[simp]
 theorem single_eq_same : (single a b : α →₀ M) a = b := by
@@ -335,7 +335,7 @@ theorem single_eq_of_ne (h : a ≠ a') : (single a b : α →₀ M) a' = 0 := by
 
 theorem single_eq_update [DecidableEq α] (a : α) (b : M) :
     ⇑(single a b) = Function.update (0 : _) a b :=
-  by classical rw [single_eq_indicator, ← Set.piecewise_eq_indicator, Set.piecewise_singleton]
+  by classical rw [single_eq_set_indicator, ← Set.piecewise_eq_indicator, Set.piecewise_singleton]
 #align finsupp.single_eq_update Finsupp.single_eq_update
 
 theorem single_eq_pi_single [DecidableEq α] (a : α) (b : M) : ⇑(single a b) = Pi.single a b :=
@@ -382,7 +382,7 @@ theorem single_injective (a : α) : Function.Injective (single a : M → α →
 #align finsupp.single_injective Finsupp.single_injective
 
 theorem single_apply_eq_zero {a x : α} {b : M} : single a b x = 0 ↔ x = a → b = 0 := by
-  simp [single_eq_indicator]
+  simp [single_eq_set_indicator]
 #align finsupp.single_apply_eq_zero Finsupp.single_apply_eq_zero
 
 theorem single_apply_ne_zero {a x : α} {b : M} : single a b x ≠ 0 ↔ x = a ∧ b ≠ 0 := by
@@ -438,7 +438,8 @@ theorem support_single_disjoint {b' : M} (hb : b ≠ 0) (hb' : b' ≠ 0) {i j :
 #align finsupp.support_single_disjoint Finsupp.support_single_disjoint
 
 @[simp]
-theorem single_eq_zero : single a b = 0 ↔ b = 0 := by simp [FunLike.ext_iff, single_eq_indicator]
+theorem single_eq_zero : single a b = 0 ↔ b = 0 := by
+  simp [FunLike.ext_iff, single_eq_set_indicator]
 #align finsupp.single_eq_zero Finsupp.single_eq_zero
 
 theorem single_swap (a₁ a₂ : α) (b : M) : single a₁ b a₂ = single a₂ b a₁ := by

Mathlib/Data/Finsupp/Indicator.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 
 ! This file was ported from Lean 3 source module data.finsupp.indicator
-! leanprover-community/mathlib commit f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
+! leanprover-community/mathlib commit 842328d9df7e96fd90fc424e115679c15fb23a71
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -74,4 +74,10 @@ theorem support_indicator_subset : ((indicator s f).support : Set ι) ⊆ s := b
   exact hi (indicator_of_not_mem h _)
 #align finsupp.support_indicator_subset Finsupp.support_indicator_subset
 
+lemma single_eq_indicator (b : α) : single i b = indicator {i} (fun _ _ => b) := by
+  classical
+  ext j
+  simp [single_apply, indicator_apply, @eq_comm _ j]
+#align finsupp.single_eq_indicator Finsupp.single_eq_indicator
+
 end Finsupp