From 111fcea7af09d0272b3fcf518e633f2e8a4f53a2 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Mon, 9 Sep 2024 13:17:12 +0200 Subject: [PATCH] Update holomorphic_JensenFormula2.lean --- Nevanlinna/holomorphic_JensenFormula2.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Nevanlinna/holomorphic_JensenFormula2.lean b/Nevanlinna/holomorphic_JensenFormula2.lean index 6402001..a267992 100644 --- a/Nevanlinna/holomorphic_JensenFormula2.lean +++ b/Nevanlinna/holomorphic_JensenFormula2.lean @@ -74,7 +74,6 @@ noncomputable def order exact B.order.toNat - theorem jensen_case_R_eq_one (f : ℂ → ℂ) (h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z)