feat(Analysis/Meromorphic): const_smul lemma (leanprover-community#39833)

This allows more general scalar type than the existing `smul` ones

Author: wwylele

Mathlib/Analysis/Meromorphic/Basic.lean

@@ -29,6 +29,7 @@ open scoped Topology
 
 variable {𝕜 𝕜' : Type*} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜']
   [NormedAlgebra 𝕜 𝕜'] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+variable {R : Type*} [NormedRing R] [Module R E] [IsBoundedSMul R E] [SMulCommClass 𝕜 R E]
 
 /-- Meromorphy of `f` at `x` (more precisely, on a punctured neighbourhood of `x`; the value at
 `x` itself is irrelevant). -/
@@ -94,6 +95,12 @@ lemma smul {f : 𝕜 → 𝕜} {g : 𝕜 → E} (hf : MeromorphicAt f x) (hg : M
   simp
   module
 
+@[to_fun (attr := fun_prop)]
+lemma const_smul {x : 𝕜} {f : 𝕜 → E} (hf : MeromorphicAt f x) (c : R) :
+    MeromorphicAt (c • f) x := by
+  rcases hf with ⟨m, hf⟩
+  exact ⟨m, by simpa [smul_comm _ c _] using hf.fun_const_smul⟩
+
 @[to_fun (attr := fun_prop)]
 lemma mul {f g : 𝕜 → 𝕜'} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
     MeromorphicAt (f * g) x := by
@@ -550,6 +557,9 @@ include hf in
     MeromorphicOn (s • f) U :=
   fun x hx ↦ (hs x hx).smul (hf x hx)
 
+include hf in
+@[to_fun] lemma const_smul (c : R) : MeromorphicOn (c • f) U := fun x hx ↦ (hf x hx).const_smul c
+
 include hs ht in
 @[to_fun] lemma mul : MeromorphicOn (s * t) U := fun x hx ↦ (hs x hx).mul (ht x hx)
 
@@ -695,6 +705,10 @@ lemma sub (hf : Meromorphic f) (hg : Meromorphic g) :
 lemma smul {f : 𝕜 → 𝕜} (hf : Meromorphic f) (hg : Meromorphic g) :
     Meromorphic (f • g) := fun x ↦ (hf x).smul (hg x)
 
+@[to_fun (attr := fun_prop)]
+lemma const_smul (hf : Meromorphic f) (c : R) :
+    Meromorphic (c • f) := fun x ↦ (hf x).const_smul c
+
 @[to_fun (attr := fun_prop)]
 lemma mul {f g : 𝕜 → 𝕜'} (hf : Meromorphic f) (hg : Meromorphic g) :
     Meromorphic (f * g) := fun x ↦ (hf x).mul (hg x)