Update Basic.lean

Aristotle/Basic.lean

@@ -7,9 +7,16 @@ variable
   {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
   {U : Set 𝕜} {f g : 𝕜 → E} {a : WithTop E} {a₀ : E}
 
-/-- Finite sums of meromorphic functions are meromorphic. -/
+/-- Derivatives of meromorphic functions are meromorphic. -/
 @[fun_prop]
-theorem MeromorphicAt.sum {ι : Type*} {s : Finset ι} {f : ι → 𝕜 → E} {x : 𝕜}
-    (h : ∀ σ, MeromorphicAt (f σ) x) :
-    MeromorphicAt (∑ n ∈ s, f n) x := by
+theorem meromorphicAt_deriv {f : 𝕜 → E} {x : 𝕜}
+    (h : MeromorphicAt f x) :
+    MeromorphicAt (deriv f) x := by
+  sorry
+
+/-- Logarithmic derivatives of meromorphic functions are meromorphic. -/
+@[fun_prop]
+theorem MeromorphicAt.logDeriv {f : 𝕜 → 𝕜} {x : 𝕜}
+    (h : MeromorphicAt f x) :
+    MeromorphicAt (f⁻¹ * deriv f) x := by
   sorry