From 4b25e0694c0aaba27658e2daa4cf116d5c5ad859 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Fri, 16 Aug 2024 07:13:38 +0200
Subject: [PATCH] Create holomorphic_zero.lean

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

diff --git a/Nevanlinna/holomorphic_zero.lean b/Nevanlinna/holomorphic_zero.lean
new file mode 100644
index 0000000..94899df
--- /dev/null
+++ b/Nevanlinna/holomorphic_zero.lean
@@ -0,0 +1,10 @@
+import Nevanlinna.holomorphic
+
+
+def zeroDivisor
+  {f : ℂ → ℂ}
+  {R : ℝ}
+  (h₁f : ∀ z ∈ Metric.closedBall z R, HolomorphicAt f z)
+  (h₂f : ∃ z ∈ Metric.closedBall z R, f z ≠ 0) :
+  ℂ → ℕ := by
+  sorry