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