chore(algebra/indicator_function): add `finset.sum_indicator_eq_sum_f…

…ilter` (#9208)

src/algebra/indicator_function.lean

@@ -248,9 +248,13 @@ section distrib_mul_action
 
 variables {A : Type*} [add_monoid A] [monoid M] [distrib_mul_action M A]
 
+lemma indicator_smul_apply (s : set α) (r : M) (f : α → A) (x : α) :
+  indicator s (λ x, r • f x) x = r • indicator s f x :=
+by { dunfold indicator, split_ifs, exacts [rfl, (smul_zero r).symm] }
+
 lemma indicator_smul (s : set α) (r : M) (f : α → A) :
   indicator s (λ (x : α), r • f x) = λ (x : α), r • indicator s f x :=
-by { simp only [indicator], funext, split_ifs, refl, exact (smul_zero r).symm }
+funext $ indicator_smul_apply s r f
 
 end distrib_mul_action
 
@@ -330,6 +334,17 @@ the same as summing the original function over the original
 `finset`. -/
 add_decl_doc sum_indicator_subset
 
+@[to_additive] lemma _root_.finset.prod_mul_indicator_eq_prod_filter
+  (s : finset ι) (f : ι → α → M) (t : ι → set α) (g : ι → α) :
+  ∏ i in s, mul_indicator (t i) (f i) (g i) = ∏ i in s.filter (λ i, g i ∈ t i), f i (g i) :=
+begin
+  refine (finset.prod_filter_mul_prod_filter_not s (λ i, g i ∈ t i) _).symm.trans _,
+  refine eq.trans _ (mul_one _),
+  exact congr_arg2 (*)
+    (finset.prod_congr rfl $ λ x hx, mul_indicator_of_mem (finset.mem_filter.1 hx).2 _)
+    (finset.prod_eq_one $ λ x hx, mul_indicator_of_not_mem (finset.mem_filter.1 hx).2 _)
+end
+
 @[to_additive] lemma mul_indicator_finset_prod (I : finset ι) (s : set α) (f : ι → α → M) :
   mul_indicator s (∏ i in I, f i) = ∏ i in I, mul_indicator s (f i) :=
 (mul_indicator_hom M s).map_prod _ _