From 67b78ad72def7e32574d26b45ad14d2d4fb5f455 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Tue, 8 Oct 2024 09:35:17 +0200
Subject: [PATCH] Add file

---
 Nevanlinna/stronglyMeromorphic.lean | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 Nevanlinna/stronglyMeromorphic.lean

diff --git a/Nevanlinna/stronglyMeromorphic.lean b/Nevanlinna/stronglyMeromorphic.lean
new file mode 100644
index 0000000..6f3f4a9
--- /dev/null
+++ b/Nevanlinna/stronglyMeromorphic.lean
@@ -0,0 +1,21 @@
+import Mathlib.Analysis.Analytic.Meromorphic
+import Nevanlinna.analyticAt
+
+def StronglyMeromorphicAt
+  (f : ℂ → ℂ)
+  (z₀ : ℂ) :=
+  (∀ᶠ (z : ℂ) in nhds z₀, f z = 0) ∨ (∃ (n : ℕ), ∃ g : ℂ → ℂ, (AnalyticAt ℂ g z₀) ∧ (g z₀ ≠ 0) ∧ (∀ᶠ (z : ℂ) in nhds z₀, f z = (z - z₀) ^ n • g z))
+
+def MeromorphicAt.makeStronglyMeromorphic
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : MeromorphicAt f z₀) :
+  ℂ → ℂ := by
+  exact 0
+
+theorem makeStronglyMeromorphic
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : MeromorphicAt f z₀) :
+  StronglyMeromorphicAt hf.makeStronglyMeromorphic z₀ := by
+  sorry