[Merged by Bors] - feat(Algebra.IndicatorFunction): indicator of smul in a SMulWithZero context

Mathlib/Algebra/IndicatorFunction.lean

@@ -511,6 +511,30 @@ theorem indicator_const_smul (s : Set α) (r : M) (f : α → A) :
 
 end DistribMulAction
 
+section SMulWithZero
+
+variable {A : Type _} [Zero A] [Zero M] [SMulWithZero M A]
+
+theorem indicator_smul_apply_left (s : Set α) (r : α → M) (f : α → A) (x : α) :
+    indicator s (fun x => r x • f x) x = indicator s r x • f x := by
+  dsimp only [indicator]
+  split_ifs
+  exacts [rfl, (zero_smul _ (f x)).symm]
+
+theorem indicator_smul_left (s : Set α) (r : α → M) (f : α → A) :
+    (indicator s fun x : α => r x • f x) = fun x : α => indicator s r x • f x :=
+  funext <| indicator_smul_apply_left s r f
+
+theorem indicator_smul_const_apply (s : Set α) (r : α → M) (a : A) (x : α) :
+    indicator s (fun x => r x • a) x = indicator s r x • a :=
+  indicator_smul_apply_left s r (fun _ => a) x
+
+theorem indicator_smul_const (s : Set α) (r : α → M) (a : A) :
+    (indicator s fun x : α => r x • a) = fun x : α => indicator s r x • a :=
+  funext <| indicator_smul_const_apply s r a
+
+end SMulWithZero
+
 section Group
 
 variable {G : Type _} [Group G] {s t : Set α} {f g : α → G} {a : α}

Mathlib/Algebra/Support.lean

@@ -217,6 +217,12 @@ theorem mulSupport_comp_eq (g : M → N) (hg : ∀ {x}, g x = 1 ↔ x = 1) (f :
 #align function.mul_support_comp_eq Function.mulSupport_comp_eq
 #align function.support_comp_eq Function.support_comp_eq
 
+@[to_additive]
+theorem mulSupport_comp_eq_of_range_subset {g : M → N} {f : α → M}
+    (hg : ∀ {x}, x ∈ range f → (g x = 1 ↔ x = 1)) :
+    mulSupport (g ∘ f) = mulSupport f :=
+  Set.ext fun x ↦ not_congr <| by rw [Function.comp, hg (mem_range_self x)]
+
 @[to_additive]
 theorem mulSupport_comp_eq_preimage (g : β → M) (f : α → β) :
     mulSupport (g ∘ f) = f ⁻¹' mulSupport g :=