feat(Topology/Algebra/Monoid): add ContinuousOn.comp_mul_left and ContinuousOn.comp_mul_right

Author: Deep0Thinking

Mathlib/Topology/Algebra/Monoid.lean

@@ -70,6 +70,18 @@ theorem continuous_mul_left (a : M) : Continuous fun b : M => a * b := by fun_pr
 @[to_additive (attr := continuity)]
 theorem continuous_mul_right (a : M) : Continuous fun b : M => b * a := by fun_prop
 
+@[to_additive]
+theorem ContinuousOn.comp_mul_left
+    {β : Type*} [TopologicalSpace β] {f : M → β} {s t : Set M} {c : M} (hf : ContinuousOn f t)
+    (hct : Set.MapsTo (fun x : M => c * x) s t) : ContinuousOn (fun x => f (c * x)) s := 
+  hf.comp (continuous_mul_left c).continuousOn hct
+
+@[to_additive]
+theorem ContinuousOn.comp_mul_right
+    {β : Type*} [TopologicalSpace β] {f : M → β} {s t : Set M} {c : M} (hf : ContinuousOn f t)
+    (hct : Set.MapsTo (fun x : M => x * c) s t) : ContinuousOn (fun x => f (x * c)) s := 
+  hf.comp (continuous_mul_right c).continuousOn hct
+
 @[to_additive]
 theorem tendsto_mul {a b : M} : Tendsto (fun p : M × M => p.fst * p.snd) (𝓝 (a, b)) (𝓝 (a * b)) :=
   continuous_iff_continuousAt.mp ContinuousMul.continuous_mul (a, b)