diff --git a/Aristotle/Basic.lean b/Aristotle/Basic.lean index 47af439..0e1b0e8 100644 --- a/Aristotle/Basic.lean +++ b/Aristotle/Basic.lean @@ -4,5 +4,5 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] lemma MeromorphicAt.comp {x : ℝ} {f : ℂ → E} {g : ℝ → ℂ} - (hf : MeromorphicAt f (g x)) (hg : MeromorphicAt g x) : MeromorphicAt (f ∘ g) x := by + (hf : MeromorphicAt f (g x)) (hg : AnalyticAt ℝ g x) : MeromorphicAt (f ∘ g) x := by sorry